Documentation

Elligator.FiniteFieldBasic

source
theorem FiniteFieldBasic.q_ne_two (q : ℕ) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
q ≠ 2
source
theorem FiniteFieldBasic.q_mod_2_congruent_1 (q : ℕ) (q_mod_4_congruent_3 : q % 4 = 3) :
q % 2 = 1
source
theorem FiniteFieldBasic.q_odd {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
Odd (Fintype.card F)
source
theorem FiniteFieldBasic.q_add_one_even {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
Even (q + 1)
source
theorem FiniteFieldBasic.q_sub_one_even {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
Even (Fintype.card F - 1)
source
theorem FiniteFieldBasic.q_sub_one_dvd_two {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
2 ∣ Fintype.card F - 1
source
theorem FiniteFieldBasic.q_not_dvd_two {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
¬2 ∣ q
source
theorem FiniteFieldBasic.power_odd_p_odd (p k : ℕ) (hk : 0 < k) (hp : Odd (p ^ k)) :
Odd p
source
theorem FiniteFieldBasic.odd_prime_power_gt_two (q : ℕ) (q_prime_power : IsPrimePow q) (hq : Odd q) :
q > 2
source
theorem FiniteFieldBasic.one_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
1 ≠ 0
source
theorem FiniteFieldBasic.q_add_one_over_four_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
(1 + q) / 4 ≠ 0
source
theorem FiniteFieldBasic.q_add_one_over_two_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
(1 + q) / 2 ≠ 0
source
theorem FiniteFieldBasic.char_ne_two {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
Fintype.card F ≠ 2
source
theorem FiniteFieldBasic.ring_char_ne_two {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
ringChar F ≠ 2
source
theorem FiniteFieldBasic.two_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
2 ≠ 0
source
theorem FiniteFieldBasic.four_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
4 ≠ 0
source
theorem FiniteFieldBasic.neg_one_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
-1 ≠ 0
source
theorem FiniteFieldBasic.neg_one_non_square {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
¬IsSquare (-1)
source
theorem FiniteFieldBasic.p_odd_power_odd (p k : ℕ) (hp : Odd p) :
Odd (p ^ k)
source
theorem FiniteFieldBasic.q_sub_one_over_two_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
(q - 1) / 2 ≠ 0
source
theorem FiniteFieldBasic.pow_two_ne_zero {F : Type u_1} [Field F] [Fintype F] {a : F} (a_ne_zero : a ≠ 0) :
a ^ 2 ≠ 0
source
theorem FiniteFieldBasic.one_sub_t_ne_zero {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) :
1 - ↑t ≠ 0
source
theorem FiniteFieldBasic.one_add_t_ne_zero {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) :
1 + ↑t ≠ 0
source
theorem FiniteFieldBasic.zero_h1 {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
0 ≠ 1 ∧ 0 ≠ -1
source
theorem FiniteFieldBasic.neg_t_ne_one_and_neg_t_ne_neg_one {F : Type u_1} [Field F] [Fintype F] (t : { t : F // t ≠ 1 ∧ t ≠ -1 }) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :
have t1 := ↑t; have t2 := -t1; t2 ≠ 1 ∧ t2 ≠ -1
source
theorem FiniteFieldBasic.one_add_card_mod_four_eq_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_mod_4_congruent_3 : q % 4 = 3) :
(1 + Fintype.card F) % 4 = 0
source
theorem FiniteFieldBasic.four_dvd_one_add_card {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_mod_4_congruent_3 : q % 4 = 3) :
4 ∣ 1 + Fintype.card F
source
theorem FiniteFieldBasic.one_add_card_over_four_mul_two_eq_one_add_card_over_two {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_mod_4_congruent_3 : q % 4 = 3) :
have card := Fintype.card F; (1 + card) / 4 * 2 = (1 + card) / 2
source
theorem FiniteFieldBasic.one_add_one_a_pow_two_eq_a_add_one_over_a_over_a {F : Type u_1} [Field F] [Fintype F] (a : F) (a_ne_zero : a ≠ 0) :
1 + 1 / a ^ 2 = (a + 1 / a) / a
source
theorem FiniteFieldBasic.card_sub_one_over_four_mul_two_eq_one_add_card_over_two {q : ℕ} :
(q - 1) / 2 = (q + 1) / 2 - 1
source
theorem FiniteFieldBasic.ringChar_of_F_eq_q {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (field_cardinality : Fintype.card F = q) (q_prime : Prime q) :
ringChar F = q
source
theorem FiniteFieldBasic.CharP_of_F_eq_q {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (field_cardinality : Fintype.card F = q) (q_prime : Prime q) :
CharP F q
source
theorem FiniteFieldBasic.exists_nat_cast_eq {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (field_cardinality : Fintype.card F = q) (q_prime : Prime q) (t : F) :
∃ n < q, ↑n = t
source
theorem FiniteFieldBasic.nat_or_neg_in_lower_half {q : ℕ} (q_prime : Prime q) (q_mod_4_congruent_3 : q % 4 = 3) (n : ℕ) (hn : n < q) :
n ≤ (q - 1) / 2 ∨ q - n ≤ (q - 1) / 2 ∧ 0 < n
source
theorem FiniteFieldBasic.neg_natCast_eq {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (field_cardinality : Fintype.card F = q) (q_prime : Prime q) (n : ℕ) (hn : 0 < n) (hn' : n < q) :
-↑n = ↑(q - n)