Non-binary fields and polynomial utilities

This module defines NonBinaryField (fields with char ≠ 2) and provides lemmas about polynomial composition with -X and X².

class NonBinaryField (F : Type u_1) extends Field F : Type u_1

A type class for fields of characteristic ≠ 2, extending Field.

• add : F → F → F
• add_assoc (a b c : F) : a + b + c = a + (b + c)
• zero : F
• zero_add (a : F) : 0 + a = a
• add_zero (a : F) : a + 0 = a
• nsmul : ℕ → F → F
• nsmul_zero (x : F) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : F) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : F) : a + b = b + a
• mul : F → F → F
• left_distrib (a b c : F) : a * (b + c) = a * b + a * c
• right_distrib (a b c : F) : (a + b) * c = a * c + b * c
• zero_mul (a : F) : 0 * a = 0
• mul_zero (a : F) : a * 0 = 0
• mul_assoc (a b c : F) : a * b * c = a * (b * c)
• one : F
• one_mul (a : F) : 1 * a = a
• mul_one (a : F) : a * 1 = a
• natCast : ℕ → F
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → F → F
• npow_zero (x : F) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : F) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : F → F
• sub : F → F → F
• sub_eq_add_neg (a b : F) : a - b = a + -b
• zsmul : ℤ → F → F
• zsmul_zero' (a : F) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : F) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : F) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : F) : -a + a = 0
• intCast : ℤ → F
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• mul_comm (a b : F) : a * b = b * a
• inv : F → F
• div : F → F → F
• div_eq_mul_inv (a b : F) : a / b = a * b⁻¹
• zpow : ℤ → F → F
• zpow_zero' (a : F) : Field.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : F) : Field.zpow (↑n.succ) a = Field.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : F) : Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : F) (y : F), x ≠ y
• nnratCast : ℚ≥0 → F
• ratCast : ℚ → F
• mul_inv_cancel (a : F) : a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def (q : ℚ≥0) : ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → F → F
• nnqsmul_def (q : ℚ≥0) (a : F) : Field.nnqsmul q a = ↑q * a
• ratCast_def (q : ℚ) : ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → F → F
• qsmul_def (a : ℚ) (x : F) : Field.qsmul a x = ↑a * x
• char_neq_2 : 2 ≠ 0

@[simp]

theorem two_mul_inv_two {F : Type u_1} [NonBinaryField F] : 2 * 2⁻¹ = 1

@[simp]

theorem inv_two_mul_two {F : Type u_1} [NonBinaryField F] : 2⁻¹ * 2 = 1

theorem coeffs_of_comp_minus_x {F : Type u_1} [Field F] {f : Polynomial F} {n : ℕ} : (f.comp (-Polynomial.X)).coeff n = if Even n then f.coeff n else -f.coeff n

theorem comp_x_square_coeff {F : Type u_1} [Field F] {f : Polynomial F} {n : ℕ} : (f.comp (Polynomial.X * Polynomial.X)).coeff n = if Even n then f.coeff (n / 2) else 0

theorem eq_poly_deg_one {F : Type u_1} [Field F] {a b c d x₁ x₂ : F} (h1 : a + b * x₁ = c + d * x₁) (h2 : a + b * x₂ = c + d * x₂) (h1_2 : x₁ ≠ x₂) : Polynomial.C a + Polynomial.C b * Polynomial.X = Polynomial.C c + Polynomial.C d * Polynomial.X