diff_of_squarestheoremProved here from basic factspropext, Quot.sound
diff_of_squaresLean 4Proved here from basic factsFormally verified
/-- **Difference of two squares:** `a² − b² = (a − b)(a + b)` in every commutative ring.`ring` expands both sides and compares them — exactly the check you would do by hand. -/theorem diff_of_squares {R : Type*} [CommRing R] (a b : R) : a ^ 2 - b ^ 2 = (a - b) * (a + b) := by ring
sum_and_diff_of_cubestheoremProved here from basic factspropext, Quot.sound
sum_and_diff_of_cubesLean 4Proved here from basic factsFormally verified
/-- **Sum and difference of two cubes:** `a³ + b³ = (a + b)(a² − ab + b²)` and`a³ − b³ = (a − b)(a² + ab + b²)`. -/theorem sum_and_diff_of_cubes {R : Type*} [CommRing R] (a b : R) : a ^ 3 + b ^ 3 = (a + b) * (a ^ 2 - a * b + b ^ 2) ∧ a ^ 3 - b ^ 3 = (a - b) * (a ^ 2 + a * b + b ^ 2) := by constructor <;> ring
sub_dvd_pow_sub_pow'theoremProved here from basic factspropext, Quot.sound
sub_dvd_pow_sub_pow'Lean 4Proved here from basic factsFormally verified
/-- **`x − a` divides `xⁿ − aⁿ`**, by induction on `n`, using the lesson's identity`xⁿ⁺¹ − aⁿ⁺¹ = x(xⁿ − aⁿ) + aⁿ(x − a)`. (Mathlib: `sub_dvd_pow_sub_pow`.) -/theorem sub_dvd_pow_sub_pow' {R : Type*} [CommRing R] (x a : R) (n : ℕ) : x - a ∣ x ^ n - a ^ n := by induction n with | zero => simp | succ n ih => obtain ⟨q, hq⟩ := ih refine ⟨x * q + a ^ n, ?_⟩ calc x ^ (n + 1) - a ^ (n + 1) = x * (x ^ n - a ^ n) + a ^ n * (x - a) := by ring _ = x * ((x - a) * q) + a ^ n * (x - a) := by rw [hq] _ = (x - a) * (x * q + a ^ n) := by ring
remainder_theoremtheoremProved here from basic factspropext, Classical.choice, Quot.sound
remainder_theoremLean 4Proved here from basic factsFormally verified
/-- **Remainder theorem:** `X − a` divides `p − p(a)`, so `p = (X − a)·q + p(a)`.As in the lesson: `p − p(a)` is a sum of terms `c (Xᵏ − aᵏ)`, and `X − a` divides each of them(`sub_dvd_pow_sub_pow'`). Lean's induction principle `Polynomial.induction_on'` builds everypolynomial from single terms `c Xᵏ` by addition, so we check those two cases. -/theorem remainder_theorem {R : Type*} [CommRing R] (p : R[X]) (a : R) : X - C a ∣ p - C (p.eval a) := by induction p using Polynomial.induction_on' with | add p q hp hq => have h : p + q - C ((p + q).eval a) = (p - C (p.eval a)) + (q - C (q.eval a)) := by rw [eval_add, C_add]; ring rw [h] exact dvd_add hp hq | monomial n c => have h : monomial n c - C ((monomial n c).eval a) = C c * (X ^ n - (C a) ^ n) := by rw [eval_monomial, ← C_mul_X_pow_eq_monomial, C_mul, C_pow]; ring rw [h] exact dvd_mul_of_dvd_right (sub_dvd_pow_sub_pow' X (C a) n) (C c)
remainder_theorem_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
remainder_theorem_libraryLean 4Applies a library theoremFormally verified
/-- **Remainder theorem, Mathlib's form:** the remainder on dividing `p` by the monic polynomial`X − a` is the constant `p(a)`. This applies `Polynomial.modByMonic_X_sub_C_eq_C_eval`. -/theorem remainder_theorem_library {R : Type*} [CommRing R] (p : R[X]) (a : R) : p %ₘ (X - C a) = C (p.eval a) := modByMonic_X_sub_C_eq_C_eval p a
factor_theoremtheoremProved here from basic factspropext, Classical.choice, Quot.sound
factor_theoremLean 4Proved here from basic factsFormally verified
/-- **Factor theorem:** `X − a` divides `p` exactly when `p(a) = 0`.(→) If `p = (X − a)·q` then `p(a) = (a − a)·q(a) = 0`.(←) If `p(a) = 0`, the remainder theorem says `X − a` divides `p − 0 = p`.(Mathlib: `Polynomial.dvd_iff_isRoot`.) -/theorem factor_theorem {R : Type*} [CommRing R] (p : R[X]) (a : R) : X - C a ∣ p ↔ p.eval a = 0 := by constructor · rintro ⟨q, rfl⟩ simp · intro h have := remainder_theorem p a rwa [h, C_0, sub_zero] at this
division_existstheoremApplies a library theorempropext, Classical.choice, Quot.sound
division_existsLean 4Applies a library theoremFormally verified
/-- **Division algorithm (existence)** over a field such as `ℚ` or `ℝ`: for `d ≠ 0` there are`q` and `r` with `p = q·d + r` and `deg r < deg d` (Mathlib's `degree` of the zero polynomial is`⊥`, below every natural number, so `r = 0` is included). This applies`EuclideanDomain.div_add_mod` and `Polynomial.degree_mod_lt`. -/theorem division_exists {K : Type*} [Field K] (p d : K[X]) (hd : d ≠ 0) : ∃ q r : K[X], p = q * d + r ∧ r.degree < d.degree := ⟨p / d, p % d, by rw [mul_comm]; exact (EuclideanDomain.div_add_mod p d).symm, degree_mod_lt p hd⟩
division_uniquetheoremProved here from basic factspropext, Classical.choice, Quot.sound
division_uniqueLean 4Proved here from basic factsFormally verified
/-- **Division algorithm (uniqueness):** quotient and remainder are unique.If `q₁d + r₁ = q₂d + r₂` with both remainders of degree `< deg d`, then`(q₁ − q₂)·d = r₂ − r₁`. If `q₁ ≠ q₂`, the left side has degree `≥ deg d`, but the right side hasdegree `< deg d` — impossible. So `q₁ = q₂`, and then `r₁ = r₂`. -/theorem division_unique {K : Type*} [Field K] {d q₁ r₁ q₂ r₂ : K[X]} (h : q₁ * d + r₁ = q₂ * d + r₂) (h₁ : r₁.degree < d.degree) (h₂ : r₂.degree < d.degree) : q₁ = q₂ ∧ r₁ = r₂ := by have key : (q₁ - q₂) * d = r₂ - r₁ := by linear_combination h have hq : q₁ = q₂ := by by_contra hne have hd : d ≠ 0 := by rintro rfl simp at h₁ have hsub : q₁ - q₂ ≠ 0 := sub_ne_zero.mpr hne -- the degree of the left side is at least `deg d` have hle : d.degree ≤ ((q₁ - q₂) * d).degree := by rw [degree_mul, add_comm] exact le_add_of_nonneg_right (zero_le_degree_iff.mpr hsub) -- the degree of the right side is less than `deg d` have hlt : (r₂ - r₁).degree < d.degree := lt_of_le_of_lt (degree_sub_le r₂ r₁) (max_lt h₂ h₁) rw [key] at hle exact absurd (lt_of_le_of_lt hle hlt) (lt_irrefl _) subst hq exact ⟨rfl, by linear_combination h⟩
card_roots_le_natDegreetheoremProved here from basic factspropext, Classical.choice, Quot.sound
card_roots_le_natDegreeLean 4Proved here from basic factsFormally verified
/-- **A non-zero polynomial of degree `n` has at most `n` roots** (over any integral domain:`ℤ`, `ℚ`, `ℝ`, `ℂ`, …). If `S` is a finite set of roots of `p ≠ 0`, then `|S| ≤ deg p`.Proof by induction on `S`, as in the lesson: if `a` is a root, the factor theorem gives`p = (X − a)·q` with `deg q = deg p − 1`; every *other* root `b` of `p` satisfies`(b − a)·q(b) = 0` with `b − a ≠ 0`, so `q(b) = 0` (zero-product property); induction on `q`finishes. -/theorem card_roots_le_natDegree {R : Type*} [CommRing R] [IsDomain R] [DecidableEq R] (S : Finset R) : ∀ p : R[X], p ≠ 0 → (∀ a ∈ S, p.eval a = 0) → S.card ≤ p.natDegree := by induction S using Finset.induction_on with | empty => intro p _ _; simp | insert a S haS ih => intro p hp hroots obtain ⟨q, rfl⟩ := (factor_theorem p a).mpr (hroots a (Finset.mem_insert_self a S)) have hq : q ≠ 0 := by rintro rfl simp at hp -- every other root of `p` is a root of `q` have hS : ∀ b ∈ S, q.eval b = 0 := by intro b hb have hb' := hroots b (Finset.mem_insert_of_mem hb) rw [eval_mul, eval_sub, eval_X, eval_C] at hb' have hba : b - a ≠ 0 := sub_ne_zero.mpr (fun h => haS (h ▸ hb)) exact (mul_eq_zero.mp hb').resolve_left hba have hdeg : ((X - C a) * q).natDegree = q.natDegree + 1 := by rw [natDegree_mul (X_sub_C_ne_zero a) hq, natDegree_X_sub_C, add_comm] rw [Finset.card_insert_of_notMem haS, hdeg] exact Nat.succ_le_succ (ih q hq hS)
eq_of_agreetheoremProved here from basic factspropext, Classical.choice, Quot.sound
eq_of_agreeLean 4Proved here from basic factsFormally verified
/-- **Identity theorem:** if two polynomials of degree `≤ n` agree at `n + 1` different points,they are the same polynomial. Their difference has degree `≤ n` and at least `n + 1` roots, so by`card_roots_le_natDegree` it must be the zero polynomial. -/theorem eq_of_agree {R : Type*} [CommRing R] [IsDomain R] [DecidableEq R] {p q : R[X]} {n : ℕ} (hp : p.natDegree ≤ n) (hq : q.natDegree ≤ n) (S : Finset R) (hS : n + 1 ≤ S.card) (hagree : ∀ a ∈ S, p.eval a = q.eval a) : p = q := by by_contra hne have hsub : p - q ≠ 0 := sub_ne_zero.mpr hne have hroots : ∀ a ∈ S, (p - q).eval a = 0 := by intro a ha rw [eval_sub, hagree a ha, sub_self] have h1 := card_roots_le_natDegree S (p - q) hsub hroots have h2 : (p - q).natDegree ≤ n := (natDegree_sub_le p q).trans (max_le hp hq) omega
two_roots_mod_seventheoremProved here from basic factspropext, Classical.choice, Quot.sound
two_roots_mod_sevenLean 4Proved here from basic factsFormally verified
/-- **Contrast:** modulo the prime 7 there are no zero divisors, and `x² − 1` has only the tworoots `1` and `6 = −1`, as the root bound predicts. `decide` checks all seven residues. -/theorem two_roots_mod_seven : ∀ x : ZMod 7, x ^ 2 - 1 = 0 ↔ x = 1 ∨ x = 6 := by decide
/-- Show that `x − a` divides `xⁿ − aⁿ` in every commutative ring.Hint: `induction n with`, and in the successor case use the identity`xⁿ⁺¹ − aⁿ⁺¹ = x(xⁿ − aⁿ) + aⁿ(x − a)`; `obtain ⟨q, hq⟩ := ih` unpacks the divisibility. -/theorem sub_dvd_pow_sub_pow' {R : Type*} [CommRing R] (x a : R) (n : ℕ) : x - a ∣ x ^ n - a ^ n := by sorry
Show the compiled solution
sub_dvd_pow_sub_pow'Lean 4Proved here from basic factsFormally verified
/-- **`x − a` divides `xⁿ − aⁿ`**, by induction on `n`, using the lesson's identity`xⁿ⁺¹ − aⁿ⁺¹ = x(xⁿ − aⁿ) + aⁿ(x − a)`. (Mathlib: `sub_dvd_pow_sub_pow`.) -/theorem sub_dvd_pow_sub_pow' {R : Type*} [CommRing R] (x a : R) (n : ℕ) : x - a ∣ x ^ n - a ^ n := by induction n with | zero => simp | succ n ih => obtain ⟨q, hq⟩ := ih refine ⟨x * q + a ^ n, ?_⟩ calc x ^ (n + 1) - a ^ (n + 1) = x * (x ^ n - a ^ n) + a ^ n * (x - a) := by ring _ = x * ((x - a) * q) + a ^ n * (x - a) := by rw [hq] _ = (x - a) * (x * q + a ^ n) := by ring
/-- Show that modulo 7 the polynomial `x² − 1` has exactly the roots `1` and `6`.Hint: there are only seven cases, and Lean can check them all for you. -/theorem two_roots_mod_seven : ∀ x : ZMod 7, x ^ 2 - 1 = 0 ↔ x = 1 ∨ x = 6 := by sorry
Show the compiled solution
two_roots_mod_sevenLean 4Proved here from basic factsFormally verified
/-- **Contrast:** modulo the prime 7 there are no zero divisors, and `x² − 1` has only the tworoots `1` and `6 = −1`, as the root bound predicts. `decide` checks all seven residues. -/theorem two_roots_mod_seven : ∀ x : ZMod 7, x ^ 2 - 1 = 0 ↔ x = 1 ∨ x = 6 := by decide