theorem FiniteFieldBasic.q_ne_two (q : ℕ) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : q ≠ 2

theorem FiniteFieldBasic.q_mod_2_congruent_1 (q : ℕ) (q_mod_4_congruent_3 : q % 4 = 3) : q % 2 = 1

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)

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)

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)

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

theorem FiniteFieldBasic.power_odd_p_odd (p k : ℕ) (hk : 0 < k) (hp : Odd (p ^ k)) : Odd p

theorem FiniteFieldBasic.odd_prime_power_gt_two (q : ℕ) (q_prime_power : IsPrimePow q) (hq : Odd q) : q > 2

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

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

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)

theorem FiniteFieldBasic.p_odd_power_odd (p k : ℕ) (hp : Odd p) : Odd (p ^ k)

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