neg_one_not_squaretheoremProved here from basic factspropext, Classical.choice, Quot.sound
neg_one_not_squareLean 4Proved here from basic factsFormally verified
/-- If `p ≡ 3 (mod 4)` then `−1` is not a square mod `p`. Proof: if `x² = −1` then, by Fermat'slittle theorem, `1 = x^(p−1) = (x²)^((p−1)/2) = (−1)^((p−1)/2) = −1`, because `(p − 1)/2` isodd; so `2 = 0` in `ℤ/pℤ`, i.e. `p ∣ 2`, which is impossible for `p ≡ 3 (mod 4)`.So `x² + 1` has no root mod `p`: the prime `p` stays prime in `ℤ[i]`. -/theorem neg_one_not_square (p : ℕ) [Fact p.Prime] (hp : p % 4 = 3) : ¬ IsSquare (-1 : ZMod p) := by rintro ⟨x, hx⟩ have hx0 : x ≠ 0 := by rintro rfl simp at hx have hp1 : p - 1 = 2 * ((p - 1) / 2) := by omega have h1 : x ^ (p - 1) = -1 := by rw [hp1, pow_mul, sq, ← hx] exact Odd.neg_one_pow ⟨(p - 1) / 2 / 2, by omega⟩ rw [ZMod.pow_card_sub_one_eq_one hx0] at h1 have h2 : ((2 : ℕ) : ZMod p) = 0 := by push_cast linear_combination h1 rw [ZMod.natCast_eq_zero_iff] at h2 have := (Nat.prime_dvd_prime_iff_eq Fact.out Nat.prime_two).mp h2 omega
neg_one_square_ifftheoremApplies a library theorempropext, Classical.choice, Quot.sound
neg_one_square_iffLean 4Applies a library theoremFormally verified
/-- The full splitting law for `x² + 1`: `−1` is a square mod an odd prime `p` iff`p ≢ 3 (mod 4)`. Whether `x² + 1` factors mod `p` depends only on `p mod 4` — the simplestreciprocity law. This applies Mathlib's `ZMod.exists_sq_eq_neg_one_iff`. -/theorem neg_one_square_iff (p : ℕ) [Fact p.Prime] : IsSquare (-1 : ZMod p) ↔ p % 4 ≠ 3 := ZMod.exists_sq_eq_neg_one_iff
sum_two_squares_mod_fourtheoremProved here from basic factspropext, Classical.choice, Quot.sound
sum_two_squares_mod_fourLean 4Proved here from basic factsFormally verified
/-- An odd prime that is a sum of two squares is `≡ 1 (mod 4)`: squares are `0` or `1` mod `4`,so a sum of two squares is never `3` mod `4`. (A prime `p = a² + b² = (a + bi)(a − bi)` splits in`ℤ[i]`.) -/theorem sum_two_squares_mod_four (p a b : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (h : a ^ 2 + b ^ 2 = p) : p % 4 = 1 := by have hodd : p % 2 = 1 := (hp.eq_two_or_odd).resolve_left hp2 have : (a ^ 2 + b ^ 2) % 4 ≠ 3 := by have ha := Nat.mod_lt a (by norm_num : 4 > 0) have hb := Nat.mod_lt b (by norm_num : 4 > 0) rw [Nat.add_mod, Nat.pow_mod, Nat.pow_mod b] interval_cases (a % 4) <;> interval_cases (b % 4) <;> norm_num omega
fermat_two_squarestheoremApplies a library theorempropext, Classical.choice, Quot.sound
fermat_two_squaresLean 4Applies a library theoremFormally verified
/-- **Fermat's two-squares theorem** (stated by Fermat, proved by Euler): a prime `p ≢ 3 (mod 4)`is a sum of two squares. With `sum_two_squares_mod_four`, a prime splits in `ℤ[i]` iff`p ≡ 1 (mod 4)` (or `p = 2`, which ramifies). This applies Mathlib's `Nat.Prime.sq_add_sq`. -/theorem fermat_two_squares (p : ℕ) [Fact p.Prime] (hp : p % 4 ≠ 3) : ∃ a b : ℕ, a ^ 2 + b ^ 2 = p := Nat.Prime.sq_add_sq hp
/-- The instance recording that `5` is prime, so that `ZMod 5` is a field and `legendreSym 5` makessense. -/instance fact_prime_five : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩
five_square_ifftheoremProved here from basic factspropext, Classical.choice, Quot.sound
five_square_iffLean 4Proved here from basic factsFormally verified
/-- **A reciprocity law with conductor 5.** For a prime `p ≠ 2, 5`: `5` is a square mod `p` iff`p ≡ ±1 (mod 5)`. Whether `x² − 5` factors mod `p` is decided by a congruence on `p` — thesplitting law of `ℚ(√5) ⊂ ℚ(ζ₅)`. Proof: since `5 ≡ 1 (mod 4)`, quadratic reciprocity gives`(5/p) = (p/5)`; this depends only on `p mod 5`, and the squares mod `5` are `1` and `4`. -/theorem five_square_iff (p : ℕ) [Fact p.Prime] (hp2 : p ≠ 2) (hp5 : p ≠ 5) : IsSquare ((5 : ℕ) : ZMod p) ↔ p % 5 = 1 ∨ p % 5 = 4 := by have hne : ((5 : ℕ) : ZMod p) ≠ 0 := by rw [Ne, ZMod.natCast_eq_zero_iff] intro h exact hp5 ((Nat.prime_dvd_prime_iff_eq Fact.out Nat.prime_five).mp h) rw [← legendreSym.eq_one_iff' p hne] -- reciprocity: `(5/p) = (p/5)` have hqr : legendreSym p ((5 : ℕ) : ℤ) = legendreSym 5 (p : ℤ) := by exact_mod_cast legendreSym.quadratic_reciprocity_one_mod_four (by norm_num : 5 % 4 = 1) hp2 rw [hqr, legendreSym.mod 5 (p : ℤ)] have hcast : (p : ℤ) % ((5 : ℕ) : ℤ) = ((p % 5 : ℕ) : ℤ) := by push_cast; rfl rw [hcast] have hr : p % 5 = 1 ∨ p % 5 = 2 ∨ p % 5 = 3 ∨ p % 5 = 4 := by have h5 : ¬ 5 ∣ p := fun h => hp5 ((Nat.prime_dvd_prime_iff_eq Nat.prime_five Fact.out).mp h).symm omega have hne' : ((p % 5 : ℕ) : ZMod 5) ≠ 0 := by rcases hr with h | h | h | h <;> rw [h] <;> decide rw [legendreSym.eq_one_iff' 5 hne'] -- the squares mod 5 are 1 and 4: a finite check rcases hr with h | h | h | h <;> rw [h] <;> decide
/-- The isomorphism `Gal(ℚ(ζₙ)/ℚ) ≅ (ℤ/nℤ)ˣ`, sending `σ` to the class `a` with `σ(ζₙ) = ζₙᵃ`.It exists because the cyclotomic polynomial `Φₙ` is irreducible over `ℚ`. This is Mathlib's`IsCyclotomicExtension.Rat.galEquivZMod`. -/noncomputable def cyclotomicGalois (n : ℕ) [NeZero n] (K : Type*) [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] : Gal(K/ℚ) ≃* (ZMod n)ˣ := IsCyclotomicExtension.Rat.galEquivZMod n K
cyclotomic_frobeniustheoremApplies a library theorempropext, Classical.choice, Quot.sound
cyclotomic_frobeniusLean 4Applies a library theoremFormally verified
/-- **Reciprocity for cyclotomic fields.** Let `p ∤ n` be prime and `P` a prime of `ℚ(ζₙ)` above`p`. Under `Gal(ℚ(ζₙ)/ℚ) ≅ (ℤ/nℤ)ˣ`, the decomposition group of `P` is the cyclic subgroupgenerated by `p mod n`: the Frobenius element at `p` "is" `p mod n`. This is class field theoryfor the fields `ℚ(ζₙ)`, and by Kronecker–Weber every abelian extension of `ℚ` lies in one ofthem. This applies Mathlib's `IsCyclotomicExtension.Rat.galEquivZMod_stabilizer`. -/theorem cyclotomic_frobenius {n : ℕ} [NeZero n] (K : Type*) [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] (p : ℕ) [Fact p.Prime] (P : Ideal (𝓞 K)) [P.IsMaximal] [P.LiesOver (Ideal.span {(p : ℤ)})] (hn : p.Coprime n) : (IsCyclotomicExtension.Rat.galEquivZMod n K).mapSubgroup (MulAction.stabilizer Gal(K/ℚ) P) = Subgroup.zpowers (ZMod.unitOfCoprime p hn) := IsCyclotomicExtension.Rat.galEquivZMod_stabilizer n K p P hn
cyclotomic_residue_degreetheoremApplies a library theorempropext, Classical.choice, Quot.sound
cyclotomic_residue_degreeLean 4Applies a library theoremFormally verified
/-- For a prime `p ∤ m`, the residue degree of `p` in `ℚ(ζₘ)` is the multiplicative order of`p mod m`: `p` factors into `φ(m)/f` primes of degree `f = ord_m(p)`. This applies Mathlib's`IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd`. -/theorem cyclotomic_residue_degree {m : ℕ} [NeZero m] (p : ℕ) [Fact p.Prime] (K : Type*) [Field K] [NumberField K] [IsCyclotomicExtension {m} ℚ K] (hm : ¬ p ∣ m) : (Ideal.span {(p : ℤ)}).inertiaDegIn (𝓞 K) = orderOf (p : ZMod m) := IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd p K hm
splits_completely_ifftheoremApplies a library theorempropext, Classical.choice, Quot.sound
splits_completely_iffLean 4Applies a library theoremFormally verified
/-- The splitting law of `ℚ(ζₘ)`: a prime `p ∤ m` (unramified by `cyclotomic_unramified`) hasresidue degree `1` — it **splits completely** — iff `p ≡ 1 (mod m)`. A one-line corollary ofMathlib's `IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd`, using that an element of agroup has order `1` iff it is the identity (`orderOf_eq_one_iff`). -/theorem splits_completely_iff {m : ℕ} [NeZero m] (p : ℕ) [Fact p.Prime] (K : Type*) [Field K] [NumberField K] [IsCyclotomicExtension {m} ℚ K] (hm : ¬ p ∣ m) : (Ideal.span {(p : ℤ)}).inertiaDegIn (𝓞 K) = 1 ↔ (p : ZMod m) = 1 := by rw [IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd p K hm, orderOf_eq_one_iff]
dirichlet_primes_in_aptheoremApplies a library theorempropext, Classical.choice, Quot.sound
dirichlet_primes_in_apLean 4Applies a library theoremFormally verified
/-- **Dirichlet's theorem** (1837): every invertible residue class `a mod q` contains infinitelymany primes. Its proof is the non-vanishing of `L(1, χ)` for the Dirichlet characters `χ mod q`— the automorphic forms for `GL(1)` over `ℚ`. In Galois terms, every element of`Gal(ℚ(ζ_q)/ℚ)` is a Frobenius element infinitely often (the abelian case of Chebotarev).This applies Mathlib's `Nat.forall_exists_prime_gt_and_eq_mod`. -/theorem dirichlet_primes_in_ap {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) (n : ℕ) : ∃ p > n, p.Prime ∧ (p : ZMod q) = a := Nat.forall_exists_prime_gt_and_eq_mod ha n
modular_transformationtheoremApplies a library theorempropext, Classical.choice, Quot.sound
modular_transformationLean 4Applies a library theoremFormally verified
/-- The defining symmetry of a **modular form** of weight `k` for `SL(2, ℤ)`:`f((az + b)/(cz + d)) = (cz + d)^k f(z)` for every `γ = (a b; c d) ∈ SL(2, ℤ)` and every `z` inthe upper half-plane (`denom γ z = cz + d`). In Mathlib a `ModularForm 𝒮ℒ k` is a holomorphicfunction on `ℍ` with this symmetry and bounded at the cusp. This applies`SlashInvariantForm.slash_action_eqn''`. -/theorem modular_transformation {k : ℤ} (f : ModularForm 𝒮ℒ k) (γ : SL(2, ℤ)) (z : UpperHalfPlane) : f (γ • z) = (UpperHalfPlane.denom γ z) ^ k * f z := SlashInvariantForm.slash_action_eqn'' f (by exact ⟨γ, rfl⟩) z
discriminant_first_coefficienttheoremApplies a library theorempropext, Classical.choice, Quot.sound
discriminant_first_coefficientLean 4Applies a library theoremFormally verified
/-- Ramanujan's cusp form `Δ(z) = q ∏ₙ (1 − qⁿ)²⁴ = Σ τ(n) qⁿ` (weight 12, level 1) isnormalised: its `q`-expansion starts `q + …`, i.e. `τ(1) = 1`. Mathlib defines `Δ` from theDedekind eta function and proves it is a cusp form. This applies`ModularForm.discriminant_qExpansion_coeff_one`. The multiplicativity of `τ` (Mordell, 1917)and Deligne's bound `|τ(p)| ≤ 2p^(11/2)` (1974) are not in Mathlib. -/theorem discriminant_first_coefficient : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ModularForm.discriminant) = 1 := ModularForm.discriminant_qExpansion_coeff_one
/-- An odd prime that is a sum of two squares is `1` mod `4`.Hint: show `(a ^ 2 + b ^ 2) % 4 ≠ 3` by splitting into the cases `a % 4` and `b % 4`(`Nat.add_mod`, `Nat.pow_mod`, `interval_cases`), then finish with `omega` using that `p` is odd(`Nat.Prime.eq_two_or_odd`). -/theorem sum_two_squares_mod_four (p a b : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (h : a ^ 2 + b ^ 2 = p) : p % 4 = 1 := by sorry
Show the compiled solution
sum_two_squares_mod_fourLean 4Proved here from basic factsFormally verified
/-- An odd prime that is a sum of two squares is `≡ 1 (mod 4)`: squares are `0` or `1` mod `4`,so a sum of two squares is never `3` mod `4`. (A prime `p = a² + b² = (a + bi)(a − bi)` splits in`ℤ[i]`.) -/theorem sum_two_squares_mod_four (p a b : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (h : a ^ 2 + b ^ 2 = p) : p % 4 = 1 := by have hodd : p % 2 = 1 := (hp.eq_two_or_odd).resolve_left hp2 have : (a ^ 2 + b ^ 2) % 4 ≠ 3 := by have ha := Nat.mod_lt a (by norm_num : 4 > 0) have hb := Nat.mod_lt b (by norm_num : 4 > 0) rw [Nat.add_mod, Nat.pow_mod, Nat.pow_mod b] interval_cases (a % 4) <;> interval_cases (b % 4) <;> norm_num omega