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

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) : ¬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.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