diff --git a/FltRegular/FltThree/Edwards.lean b/FltRegular/FltThree/Edwards.lean index ffa85ded..a8464306 100644 --- a/FltRegular/FltThree/Edwards.lean +++ b/FltRegular/FltThree/Edwards.lean @@ -15,7 +15,7 @@ theorem Zsqrtd.associated_norm_of_associated {d : ℤ} {f g : ℤ√d} (h : Asso exact associated_mul_unit_right (Zsqrtd.norm f) _ this #align zsqrtd.associated_norm_of_associated Zsqrtd.associated_norm_of_associated -theorem OddPrimeOrFour.im_ne_zero {p : ℤ√(-3)} (h : OddPrimeOrFour p.norm) +theorem OddPrimeOrFour.im_ne_zero {p : ℤ√(-3)} (h : OddPrimeOrFour p.norm.natAbs) (hcoprime : IsCoprime p.re p.im) : p.im ≠ 0 := by intro H @@ -24,7 +24,8 @@ theorem OddPrimeOrFour.im_ne_zero {p : ℤ√(-3)} (h : OddPrimeOrFour p.norm) · rw [H, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime rw [← sq_abs, hcoprime] at h norm_num at h - · exact not_prime_pow one_lt_two.ne' hp + · rw [Int.natAbs_pow] at hp + exact hp.not_prime_pow le_rfl #align odd_prime_or_four.im_ne_zero OddPrimeOrFour.im_ne_zero theorem Zsqrt3.isUnit_iff {z : ℤ√(-3)} : IsUnit z ↔ abs z.re = 1 ∧ z.im = 0 := @@ -52,22 +53,26 @@ theorem Zsqrt3.coe_of_isUnit' {z : ℤ√(-3)} (h : IsUnit z) : ∃ u : ℤ, z = · exact Int.isUnit_iff_abs_eq.mp u.isUnit #align zsqrt3.coe_of_is_unit' Zsqrt3.coe_of_isUnit' +theorem Zsqrt3.norm_natAbs (a : ℤ√(-3)) : a.norm.natAbs = a.norm := by + rw [Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)] + theorem OddPrimeOrFour.factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) - (hx : OddPrimeOrFour x) (hfactor : x ∣ a.norm) : + (hx : OddPrimeOrFour x.natAbs) (hfactor : x ∣ a.norm) : ∃ c : ℤ√(-3), |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0 := by - obtain rfl | ⟨hprime, hodd⟩ := hx + obtain hx | ⟨hprime, hodd⟩ := hx · refine' ⟨⟨1, 1⟩, _, zero_le_one, one_ne_zero⟩ - simp only [Zsqrtd.norm_def, mul_one, abs_of_pos, zero_lt_four, sub_neg_eq_add] - decide - · obtain ⟨c, hc⟩ := _root_.factors a x hcoprime hodd hfactor + simp only [Zsqrtd.norm_def, mul_one, sub_neg_eq_add, Int.abs_eq_natAbs, hx] + norm_num + · rw [Int.natAbs_odd] at hodd + obtain ⟨c, hc⟩ := _root_.factors a x hcoprime hodd hfactor rw [hc] apply Zsqrtd.exists c intro H - rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two, eq_comm] at hc - have := hprime.abs - rw [←hc] at this - exact not_prime_pow one_lt_two.ne' this + rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two, eq_comm, Int.abs_eq_natAbs] + at hc + rw [Nat.prime_iff_prime_int, ← hc] at hprime + exact not_prime_pow one_lt_two.ne' hprime #align odd_prime_or_four.factors OddPrimeOrFour.factors theorem step1a {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even a.norm) : @@ -166,54 +171,63 @@ theorem step2 {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : p.norm #align step2 step2 theorem step1_2 {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : p.norm ∣ a.norm) - (hp : OddPrimeOrFour p.norm) (hq : p.im ≠ 0) : + (hp : OddPrimeOrFour p.norm.natAbs) (hq : p.im ≠ 0) : ∃ u : ℤ√(-3), IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm := by obtain hp | ⟨hpprime, -⟩ := hp - · rw [hp] at hdvd⊢ + · replace hp : p.norm = 4 := by + rw [← Zsqrt3.norm_natAbs] + norm_cast + rw [hp] at hdvd⊢ have heven : Even a.norm := by apply even_iff_two_dvd.mpr (dvd_trans _ hdvd) norm_num exact step1'' hcoprime hp hq heven - · apply step2 hcoprime hdvd hpprime + · rw [← Int.prime_iff_natAbs_prime] at hpprime + apply step2 hcoprime hdvd hpprime #align step1_2 step1_2 theorem OddPrimeOrFour.factors' {a : ℤ√(-3)} (h2 : a.norm ≠ 1) (hcoprime : IsCoprime a.re a.im) : ∃ u q : ℤ√(-3), 0 ≤ q.re ∧ - q.im ≠ 0 ∧ OddPrimeOrFour q.norm ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm := by - have h2 : 2 < a.norm := by + q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm := + by + have h2 : 2 < a.norm.natAbs := by + zify + rw [abs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)] apply lt_of_le_of_ne _ (Spts.not_two _).symm rw [← one_mul (2 : ℤ), mul_two, Int.add_one_le_iff] apply lt_of_le_of_ne _ h2.symm rw [← Int.sub_one_lt_iff, sub_self] exact Spts.pos_of_coprime' hcoprime obtain ⟨p, hpdvd, hp⟩ := OddPrimeOrFour.exists_and_dvd h2 + rw [← Int.ofNat_dvd_left] at hpdvd obtain ⟨q', hcd, hc, hd⟩ := OddPrimeOrFour.factors a p hcoprime hp hpdvd - rw [← abs_dvd, hcd] at hpdvd - have hp' := hp.abs - rw [hcd] at hp' - obtain ⟨u, huvcoprime, huv, huvdvd⟩ := step1_2 hcoprime hpdvd hp' hd + rw [Nat.abs_cast, ← Zsqrt3.norm_natAbs, Nat.cast_inj] at hcd + rw [hcd] at hpdvd hp + rw [Int.natAbs_dvd] at hpdvd + obtain ⟨u, huvcoprime, huv, huvdvd⟩ := step1_2 hcoprime hpdvd hp hd use u cases' huv with huv huv <;> [(use q'); (use star q')] <;> simp only [IsCoprime, Zsqrtd.star_re, Zsqrtd.star_im, Ne.def, neg_eq_zero, Zsqrtd.norm_conj] <;> - use hc, hd, hp', huv, huvcoprime <;> - · rw [huvdvd, lt_mul_iff_one_lt_left (Spts.pos_of_coprime' huvcoprime), ← hcd] - exact hp.one_lt_abs + use hc, hd, hp, huv, huvcoprime <;> + · rw [huvdvd, lt_mul_iff_one_lt_left (Spts.pos_of_coprime' huvcoprime), ← Zsqrt3.norm_natAbs, + Nat.one_lt_cast] + exact hp.one_lt #align odd_prime_or_four.factors' OddPrimeOrFour.factors' theorem step3 {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : ∃ f : Multiset (ℤ√(-3)), (a = f.prod ∨ a = -f.prod) ∧ - ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm := + ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs := by suffices ∀ n : ℕ, a.norm.natAbs = n → ∃ f : Multiset (ℤ√(-3)), (a = f.prod ∨ a = -f.prod) ∧ - ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm + ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs by exact this a.norm.natAbs rfl intro n hn induction' n using Nat.strong_induction_on with n ih generalizing a @@ -239,7 +253,7 @@ theorem step3 {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : #align step3 step3 theorem step4_3 {p p' : ℤ√(-3)} (hcoprime : IsCoprime p.re p.im) (hcoprime' : IsCoprime p'.re p'.im) - (h : OddPrimeOrFour p.norm) (heq : p.norm = p'.norm) : + (h : OddPrimeOrFour p.norm.natAbs) (heq : p.norm = p'.norm) : abs p.re = abs p'.re ∧ abs p.im = abs p'.im := by have hdvd : p'.norm ∣ p.norm := by rw [heq] @@ -262,15 +276,22 @@ theorem prod_map_norm {d : ℤ} {s : Multiset (ℤ√d)} : Multiset.prod_hom s (Zsqrtd.normMonoidHom : ℤ√d →* ℤ) #align prod_map_norm prod_map_norm +theorem prod_map_natAbs {s : Multiset ℤ} : + (s.map Int.natAbs).prod = Int.natAbs s.prod := + Multiset.prod_hom s <| + ({ toFun := Int.natAbs + map_one' := rfl + map_mul' := fun x y => Int.natAbs_mul x y } : ℤ →* ℕ) + theorem factors_unique_prod : ∀ {f g : Multiset (ℤ√(-3))}, - (∀ x ∈ f, OddPrimeOrFour (Zsqrtd.norm x)) → - (∀ x ∈ g, OddPrimeOrFour (Zsqrtd.norm x)) → + (∀ x ∈ f, OddPrimeOrFour (Zsqrtd.norm x).natAbs) → + (∀ x ∈ g, OddPrimeOrFour (Zsqrtd.norm x).natAbs) → Associated f.prod.norm g.prod.norm → - Multiset.Rel Associated (f.map Zsqrtd.norm) (g.map Zsqrtd.norm) := + (f.map (Int.natAbs ∘ Zsqrtd.norm)) = (g.map (Int.natAbs ∘ Zsqrtd.norm)) := by intro f g hf hg hassoc - apply factors_unique_prod' + refine factors_unique_prod' ?_ ?_ ?_ · intro x hx rw [Multiset.mem_map] at hx obtain ⟨y, hy, rfl⟩ := hx @@ -279,7 +300,8 @@ theorem factors_unique_prod : rw [Multiset.mem_map] at hx obtain ⟨y, hy, rfl⟩ := hx exact hg y hy - · rwa [prod_map_norm, prod_map_norm] + · simp_rw [← Multiset.map_map, prod_map_natAbs, prod_map_norm, ← Int.associated_iff_natAbs] + exact hassoc #align factors_unique_prod factors_unique_prod /-- The multiset of factors. -/ @@ -291,7 +313,7 @@ noncomputable def factorization' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.i theorem factorization'_prop {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : (a = (factorization' hcoprime).prod ∨ a = -(factorization' hcoprime).prod) ∧ ∀ pq : ℤ√(-3), - pq ∈ factorization' hcoprime → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm := + pq ∈ factorization' hcoprime → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs := Classical.choose_spec (step3 hcoprime) #align factorization'_prop factorization'_prop @@ -369,7 +391,7 @@ theorem associated'_of_abs_eq {x y : ℤ√(-3)} (hre : abs x.re = abs y.re) theorem associated'_of_associated_norm {x y : ℤ√(-3)} (h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)) (hx : IsCoprime x.re x.im) - (hy : IsCoprime y.re y.im) (h' : OddPrimeOrFour x.norm) : Associated' x y := + (hy : IsCoprime y.re y.im) (h' : OddPrimeOrFour x.norm.natAbs) : Associated' x y := by have heq : x.norm = y.norm := haveI hd : (-3 : ℤ) ≤ 0 := by norm_num @@ -378,45 +400,46 @@ theorem associated'_of_associated_norm {x y : ℤ√(-3)} exact associated'_of_abs_eq hre him #align associated'_of_associated_norm associated'_of_associated_norm -theorem factorization'.associated'_of_norm_eq {a b c : ℤ√(-3)} (h : IsCoprime a.re a.im) - (hbmem : b ∈ factorization' h) (hcmem : c ∈ factorization' h) (hnorm : b.norm = c.norm) : - Associated' b c := by +theorem factorization'.associated'_of_norm_associated {a b c : ℤ√(-3)} (h : IsCoprime a.re a.im) + (hbmem : b ∈ factorization' h) (hcmem : c ∈ factorization' h) + (hnorm : Associated b.norm c.norm) : Associated' b c := by apply associated'_of_associated_norm - · rw [hnorm] + · exact hnorm · exact factorization'.coprime_of_mem h hbmem · exact factorization'.coprime_of_mem h hcmem · exact ((factorization'_prop h).2 b hbmem).2.2 -#align factorization'.associated'_of_norm_eq factorization'.associated'_of_norm_eq +#align factorization'.associated'_of_norm_eq factorization'.associated'_of_norm_associated -theorem factors_unique {f g : Multiset (ℤ√(-3))} (hf : ∀ x ∈ f, OddPrimeOrFour (Zsqrtd.norm x)) +theorem factors_unique {f g : Multiset (ℤ√(-3))} (hf : ∀ x ∈ f, OddPrimeOrFour (Zsqrtd.norm x).natAbs) (hf' : ∀ x ∈ f, IsCoprime (Zsqrtd.re x) (Zsqrtd.im x)) - (hg : ∀ x ∈ g, OddPrimeOrFour (Zsqrtd.norm x)) + (hg : ∀ x ∈ g, OddPrimeOrFour (Zsqrtd.norm x).natAbs) (hg' : ∀ x ∈ g, IsCoprime (Zsqrtd.re x) (Zsqrtd.im x)) (h : Associated f.prod g.prod) : Multiset.Rel Associated' f g := by have p : ∀ (x : ℤ√(-3)) (_ : x ∈ f) (y : ℤ√(-3)) (_ : y ∈ g), - Associated x.norm y.norm → Associated' x y := + (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y := by intro x hx y hy hxy + rw [Function.comp_apply, Function.comp_apply, ← Int.associated_iff_natAbs] at hxy apply associated'_of_associated_norm hxy · exact hf' x hx · exact hg' y hy · exact hf x hx refine' Multiset.Rel.mono _ p - rw [← Multiset.rel_map] - apply factors_unique_prod hf hg - exact Zsqrtd.associated_norm_of_associated h + rw [← Multiset.rel_map, factors_unique_prod hf hg <| Zsqrtd.associated_norm_of_associated h, + Multiset.rel_eq] #align factors_unique factors_unique theorem factors_2_even' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : - Even (evenFactorExp a.norm) := + Even (evenFactorExp a.norm.natAbs) := by induction' hn : a.norm.natAbs using Nat.strong_induction_on with n ih generalizing a - by_cases hparity : Even a.norm - · obtain ⟨u, huvcoprime, huvprod⟩ := step1' hcoprime hparity + by_cases hparity : Even a.norm.natAbs + · obtain ⟨u, huvcoprime, huvprod⟩ := step1' hcoprime (Int.natAbs_even.mp hparity) have huv := Spts.ne_zero_of_coprime' _ huvcoprime - rw [huvprod, factors_2_even huv, Nat.even_add] + have h₄ : Int.natAbs 4 = 4 := by norm_num; decide + rw [← hn, huvprod, Int.natAbs_mul, h₄, factors_2_even (by simpa using huv), Nat.even_add] apply iff_of_true even_two apply ih _ _ huvcoprime rfl rw [← hn, huvprod, Int.natAbs_mul, lt_mul_iff_one_lt_left (Int.natAbs_pos.mpr huv)] @@ -424,15 +447,19 @@ theorem factors_2_even' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : · convert even_zero (α := ℕ) simp only [evenFactorExp, Multiset.count_eq_zero, hn] contrapose! hparity with hfactor - rw [even_iff_two_dvd] + rw [hn, even_iff_two_dvd] exact UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors hfactor #align factors_2_even' factors_2_even' -theorem factorsOddPrimeOrFour.unique {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) {f : Multiset ℤ} - (hf : ∀ x ∈ f, OddPrimeOrFour x) (hf' : ∀ x ∈ f, (0 : ℤ) ≤ x) - (hassoc : Associated f.prod a.norm) : f = factorsOddPrimeOrFour a.norm := - factorsOddPrimeOrFour.unique' hf hf' (Spts.pos_of_coprime' hcoprime) (factors_2_even' hcoprime) - hassoc +theorem factorsOddPrimeOrFour.unique {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) {f : Multiset ℕ} + (hf : ∀ x ∈ f, OddPrimeOrFour x) (hassoc : f.prod = a.norm.natAbs) : + factorsOddPrimeOrFour a.norm.natAbs = f := by + rw [← hassoc] + refine factorsOddPrimeOrFour.unique' hf ?_ ?_ + · rw [hassoc, Int.natAbs_pos] + exact Spts.ne_zero_of_coprime' _ hcoprime + · rw [hassoc] + exact factors_2_even' hcoprime #align factors_odd_prime_or_four.unique factorsOddPrimeOrFour.unique theorem eq_or_eq_conj_of_associated_of_re_zero {x A : ℤ√(-3)} (hx : x.re = 0) (h : Associated x A) : @@ -504,14 +531,14 @@ theorem eq_or_eq_conj_iff_associated'_of_nonneg {x A : ℤ√(-3)} (hx : 0 ≤ x theorem step5' -- lemma page 54 (a : ℤ√(-3)) - (r : ℤ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = a.norm) : + (r : ℕ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = a.norm.natAbs) : ∃ g : Multiset (ℤ√(-3)), factorization' hcoprime = 3 • g := by classical obtain ⟨h1, h2⟩ := factorization'_prop hcoprime set f := factorization' hcoprime with hf apply Multiset.exists_smul_of_dvd_count intro x hx - convert dvd_mul_right 3 (Multiset.count (Zsqrtd.norm x) (factorsOddPrimeOrFour r)) + convert dvd_mul_right 3 (Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r)) have : Even (evenFactorExp r) := by suffices Even (3 * evenFactorExp r) @@ -524,35 +551,32 @@ theorem step5' calc Multiset.count x f = Multiset.card (Multiset.filter (x = ·) f) := by rw [Multiset.count, Multiset.countP_eq_card_filter] - _ = Multiset.card (Multiset.filter (fun a : ℤ√(-3) => x.norm = a.norm) f) := + _ = Multiset.card (Multiset.filter (fun a : ℤ√(-3) => x.norm.natAbs = a.norm.natAbs) f) := (congr_arg _ (Multiset.filter_congr fun A HA => ?_)) - _ = Multiset.countP (x.norm = ·) (Multiset.map Zsqrtd.norm f) := - (Multiset.countP_map Zsqrtd.norm f (x.norm = ·)).symm - _ = Multiset.countP (x.norm = ·) (factorsOddPrimeOrFour a.norm) := ?_ - _ = Multiset.count x.norm (factorsOddPrimeOrFour a.norm) := by rw [Multiset.count] - _ = Multiset.count x.norm (factorsOddPrimeOrFour (r ^ 3)) := by rw [hcube] - _ = Multiset.count x.norm (3 • _) := (congr_arg _ <| factorsOddPrimeOrFour.pow _ _ this) - _ = 3 * _ := Multiset.count_nsmul x.norm _ _ + _ = Multiset.countP (x.norm.natAbs = ·) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) := + (Multiset.countP_map _ f (x.norm.natAbs = ·)).symm + _ = Multiset.countP (x.norm.natAbs = ·) ((factorsOddPrimeOrFour a.norm.natAbs)) := ?_ + _ = Multiset.count x.norm.natAbs ((factorsOddPrimeOrFour a.norm.natAbs)) := by rw [Multiset.count] + _ = Multiset.count x.norm.natAbs ((factorsOddPrimeOrFour (r ^ 3))) := by rw [hcube] + _ = Multiset.count x.norm.natAbs (3 • _) := by rw [factorsOddPrimeOrFour.pow _ _ this] + _ = 3 * _ := Multiset.count_nsmul x.norm.natAbs _ _ swap show - Multiset.countP (Eq x.norm) (Multiset.map Zsqrtd.norm f) = - Multiset.countP (Eq x.norm) (factorsOddPrimeOrFour a.norm) - congr - · apply factorsOddPrimeOrFour.unique hcoprime + Multiset.countP (Eq x.norm.natAbs) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) = + Multiset.countP (Eq x.norm.natAbs) ((factorsOddPrimeOrFour a.norm.natAbs)) + congr 1 + · rw [factorsOddPrimeOrFour.unique hcoprime] · intro x hx obtain ⟨y, hy, rfl⟩ := Multiset.mem_map.mp hx exact (h2 y hy).2.2 - · intro x hx - obtain ⟨y, -, rfl⟩ := Multiset.mem_map.mp hx - apply Zsqrtd.norm_nonneg - norm_num - · rw [prod_map_norm] + · rw [← Multiset.map_map, prod_map_natAbs, prod_map_norm] cases' h1 with h1 h1 <;> rw [h1] rw [Zsqrtd.norm_neg] have h2x := h2 x hx - refine' ⟨congr_arg _, fun h => _⟩ - have hassoc := factorization'.associated'_of_norm_eq hcoprime hx HA h + refine' ⟨fun h => by rw [h], fun h => _⟩ + rw [← Int.associated_iff_natAbs] at h + have hassoc := factorization'.associated'_of_norm_associated hcoprime hx HA h have eq_or_eq_conj := (eq_or_eq_conj_iff_associated'_of_nonneg h2x.1 (h2 A HA).1).mp hassoc refine' eq_or_eq_conj.resolve_right fun H => _ apply no_conj f @@ -570,7 +594,7 @@ theorem step5' theorem step5 -- lemma page 54 (a : ℤ√(-3)) - (r : ℤ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = a.norm) : ∃ p : ℤ√(-3), a = p ^ 3 := + (r : ℕ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = a.norm.natAbs) : ∃ p : ℤ√(-3), a = p ^ 3 := by obtain ⟨f, hf⟩ := step5' a r hcoprime hcube obtain ⟨h1, -⟩ := factorization'_prop hcoprime @@ -588,11 +612,13 @@ theorem step6 (a b r : ℤ) (hcoprime : IsCoprime a b) (hcube : r ^ 3 = a ^ 2 + ∃ p q, a = p ^ 3 - 9 * p * q ^ 2 ∧ b = 3 * p ^ 2 * q - 3 * q ^ 3 := by set A : ℤ√(-3) := ⟨a, b⟩ with hA - have hcube' : r ^ 3 = A.norm := + have hcube' : r.natAbs ^ 3 = A.norm.natAbs := by + rw [← Int.natAbs_pow] + apply congr_arg simp only [hcube, Zsqrtd.norm_def, hA] ring - obtain ⟨p, hp⟩ := step5 A r hcoprime hcube' + obtain ⟨p, hp⟩ := step5 A r.natAbs hcoprime hcube' use p.re, p.im simp only [Zsqrtd.ext, pow_succ', pow_two, Zsqrtd.mul_re, Zsqrtd.mul_im] at hp convert hp using 2 <;> simp <;> ring diff --git a/FltRegular/FltThree/OddPrimeOrFour.lean b/FltRegular/FltThree/OddPrimeOrFour.lean index b99e4132..b0303b58 100644 --- a/FltRegular/FltThree/OddPrimeOrFour.lean +++ b/FltRegular/FltThree/OddPrimeOrFour.lean @@ -4,41 +4,34 @@ Released under Apache 2.0 license as described in the file LICENSE. ! This file was ported from Lean 3 source module main -/ -import Mathlib.Data.Int.Parity import Mathlib.RingTheory.Int.Basic -import Mathlib.RingTheory.Prime /-- Being equal to `4` or odd. -/ -def OddPrimeOrFour (z : ℤ) : Prop := - z = 4 ∨ Prime z ∧ Odd z +def OddPrimeOrFour (z : ℕ) : Prop := + z = 4 ∨ Nat.Prime z ∧ Odd z #align odd_prime_or_four OddPrimeOrFour -theorem OddPrimeOrFour.ne_zero {z : ℤ} (h : OddPrimeOrFour z) : z ≠ 0 := +theorem OddPrimeOrFour.ne_zero {z : ℕ} (h : OddPrimeOrFour z) : z ≠ 0 := by obtain rfl | ⟨h, -⟩ := h · norm_num · exact h.ne_zero #align odd_prime_or_four.ne_zero OddPrimeOrFour.ne_zero -theorem OddPrimeOrFour.ne_one {z : ℤ} (h : OddPrimeOrFour z) : z ≠ 1 := +theorem OddPrimeOrFour.ne_one {z : ℕ} (h : OddPrimeOrFour z) : z ≠ 1 := by obtain rfl | ⟨h, -⟩ := h · norm_num · exact h.ne_one #align odd_prime_or_four.ne_one OddPrimeOrFour.ne_one -theorem OddPrimeOrFour.one_lt_abs {z : ℤ} (h : OddPrimeOrFour z) : 1 < abs z := +theorem OddPrimeOrFour.one_lt {z : ℕ} (h : OddPrimeOrFour z) : 1 < z := by obtain rfl | ⟨h, -⟩ := h - · rw [Int.abs_eq_natAbs] - norm_num; decide - · rw [Int.abs_eq_natAbs] - rw [Int.prime_iff_natAbs_prime] at h - norm_cast - exact h.one_lt -#align odd_prime_or_four.one_lt_abs OddPrimeOrFour.one_lt_abs + · norm_num + · exact h.one_lt -theorem OddPrimeOrFour.not_unit {z : ℤ} (h : OddPrimeOrFour z) : ¬IsUnit z := +theorem OddPrimeOrFour.not_unit {z : ℕ} (h : OddPrimeOrFour z) : ¬IsUnit z := by obtain rfl | ⟨h, -⟩ := h · rw [isUnit_iff_dvd_one] @@ -46,83 +39,68 @@ theorem OddPrimeOrFour.not_unit {z : ℤ} (h : OddPrimeOrFour z) : ¬IsUnit z := · exact h.not_unit #align odd_prime_or_four.not_unit OddPrimeOrFour.not_unit -theorem OddPrimeOrFour.abs {z : ℤ} (h : OddPrimeOrFour z) : OddPrimeOrFour (abs z) := - by - obtain rfl | ⟨hp, ho⟩ := h - · left - rw [abs_eq_self] - norm_num - · right - exact ⟨hp.abs, odd_abs.mpr ho⟩ -#align odd_prime_or_four.abs OddPrimeOrFour.abs - -theorem OddPrimeOrFour.exists_and_dvd {n : ℤ} (n2 : 2 < n) : ∃ p, p ∣ n ∧ OddPrimeOrFour p := by - lift n to ℕ using (zero_lt_two.trans n2).le - norm_cast at n2 +theorem OddPrimeOrFour.exists_and_dvd {n : ℕ} (n2 : 2 < n) : ∃ p, p ∣ n ∧ OddPrimeOrFour p := by obtain h4 | ⟨p, hpprime, hpdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt n2 - · refine ⟨4, ?_, Or.inl rfl⟩ - norm_cast - · exact ⟨p, Int.ofNat_dvd.mpr hpdvd, Or.inr ⟨Nat.prime_iff_prime_int.mp hpprime, - (Int.odd_coe_nat p).mpr hpodd⟩⟩ + · exact ⟨4, h4, Or.inl rfl⟩ + · exact ⟨p, hpdvd, Or.inr ⟨hpprime, hpodd⟩⟩ #align odd_prime_or_four.exists_and_dvd OddPrimeOrFour.exists_and_dvd -theorem associated_of_dvd {a p : ℤ} (ha : OddPrimeOrFour a) (hp : OddPrimeOrFour p) (h : p ∣ a) : - Associated p a := +theorem eq_of_dvd {a p : ℕ} (ha : OddPrimeOrFour a) (hp : OddPrimeOrFour p) (h : p ∣ a) : + p = a := by obtain rfl | ⟨ap, aodd⟩ := ha <;> obtain rfl | ⟨pp, podd⟩ := hp · rfl · exfalso - have h0 : (4 : ℤ) = 2 ^ 2 := by norm_num + have h0 : (4 : ℕ) = 2 ^ 2 := by norm_num rw [h0] at h - refine' Int.even_iff_not_odd.mp _ podd + refine' Nat.even_iff_not_odd.mp _ podd rw [even_iff_two_dvd] - apply Associated.dvd _ - exact ((pp.dvd_prime_iff_associated Int.prime_two).mp (pp.dvd_of_dvd_pow h)).symm + exact pp.dvd_symm Nat.prime_two (pp.dvd_of_dvd_pow h) · exfalso - rw [Int.odd_iff_not_even] at aodd + rw [Nat.odd_iff_not_even] at aodd refine' aodd _ rw [even_iff_two_dvd] refine' dvd_trans _ h norm_num - · rwa [Prime.dvd_prime_iff_associated pp ap] at h -#align associated_of_dvd associated_of_dvd + · rwa [Nat.prime_dvd_prime_iff_eq pp ap] at h -theorem dvd_or_dvd {a p x : ℤ} (ha : OddPrimeOrFour a) (hp : OddPrimeOrFour p) (hdvd : p ∣ a * x) : +theorem dvd_or_dvd {a p x : ℕ} (ha : OddPrimeOrFour a) (hp : OddPrimeOrFour p) (hdvd : p ∣ a * x) : p ∣ a ∨ p ∣ x := by obtain rfl | ⟨pp, -⟩ := hp · obtain rfl | ⟨ap, aodd⟩ := ha · exact Or.inl dvd_rfl · right - have : (4 : ℤ) = 2 ^ 2 := by norm_num + have : (4 : ℕ) = 2 ^ 2 := by norm_num rw [this] at hdvd⊢ - apply Int.prime_two.pow_dvd_of_dvd_mul_left _ _ hdvd - rwa [← even_iff_two_dvd, ← Int.odd_iff_not_even] - · exact pp.dvd_or_dvd hdvd + apply Nat.prime_two.prime.pow_dvd_of_dvd_mul_left _ _ hdvd + rwa [← even_iff_two_dvd, ← Nat.odd_iff_not_even] + · exact pp.dvd_mul.mp hdvd #align dvd_or_dvd dvd_or_dvd -theorem exists_associated_mem_of_dvd_prod'' {p : ℤ} (hp : OddPrimeOrFour p) {s : Multiset ℤ} - (hs : ∀ r ∈ s, OddPrimeOrFour r) (hdvd : p ∣ s.prod) : ∃ q ∈ s, Associated p q := +theorem mem_of_dvd_prod {p : ℕ} (hp : OddPrimeOrFour p) {s : Multiset ℕ} + (hs : ∀ r ∈ s, OddPrimeOrFour r) (hdvd : p ∣ s.prod) : p ∈ s := by induction' s using Multiset.induction_on with a s ih hs - · simp [hp.not_unit, ← isUnit_iff_dvd_one] at hdvd + · simp [hp.ne_one] at hdvd · rw [Multiset.prod_cons] at hdvd have := hs a (Multiset.mem_cons_self _ _) obtain h | h := dvd_or_dvd this hp hdvd - · exact ⟨a, Multiset.mem_cons_self _ _, associated_of_dvd this hp h⟩ - · obtain ⟨q, hq₁, hq₂⟩ := ih (fun r hr => hs _ (Multiset.mem_cons_of_mem hr)) h - exact ⟨q, Multiset.mem_cons_of_mem hq₁, hq₂⟩ -#align exists_associated_mem_of_dvd_prod'' exists_associated_mem_of_dvd_prod'' + · rw [eq_of_dvd this hp h] + exact Multiset.mem_cons_self _ _ + · have := ih (fun r hr => hs _ (Multiset.mem_cons_of_mem hr)) h + exact Multiset.mem_cons_of_mem this theorem factors_unique_prod' : - ∀ {f g : Multiset ℤ}, + ∀ {f g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → - (∀ x ∈ g, OddPrimeOrFour x) → Associated f.prod g.prod → Multiset.Rel Associated f g := + (∀ x ∈ g, OddPrimeOrFour x) → + f.prod = g.prod → f = g := by intro f induction' f using Multiset.induction_on with p f ih · rintro g - hg h rw [Multiset.prod_zero] at h - rw [Multiset.rel_zero_left] + symm apply Multiset.eq_zero_of_forall_not_mem intro x hx apply (hg x hx).not_unit @@ -132,20 +110,20 @@ theorem factors_unique_prod' : have hp := hf p (Multiset.mem_cons_self _ _) have hdvd : p ∣ g.prod := by - rw [← hfg.dvd_iff_dvd_right, Multiset.prod_cons] + rw [← hfg, Multiset.prod_cons] exact dvd_mul_right _ _ - obtain ⟨b, hbg, hb⟩ := exists_associated_mem_of_dvd_prod'' hp hg hdvd + have hbg := mem_of_dvd_prod hp hg hdvd rw [← Multiset.cons_erase hbg] - apply Multiset.Rel.cons hb + congr apply ih _ _ _ · exact fun q hq => hf _ (Multiset.mem_cons_of_mem hq) - · exact fun q (hq : q ∈ g.erase b) => hg q (Multiset.mem_of_mem_erase hq) - · apply Associated.of_mul_left _ hb hp.ne_zero - rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg] + · exact fun q hq => hg q (Multiset.mem_of_mem_erase hq) + · apply mul_left_cancel₀ hp.ne_zero + rwa [Multiset.prod_erase hbg, ← Multiset.prod_cons] #align factors_unique_prod' factors_unique_prod' /-- The odd factors. -/ -noncomputable def oddFactors (x : ℤ) := +noncomputable def oddFactors (x : ℕ) := Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors x) #align odd_factors oddFactors @@ -153,29 +131,22 @@ theorem oddFactors.zero : oddFactors 0 = 0 := rfl #align odd_factors.zero oddFactors.zero -theorem oddFactors.not_two_mem (x : ℤ) : (2 : ℤ) ∉ oddFactors x := by +theorem oddFactors.not_two_mem (x : ℕ) : 2 ∉ oddFactors x := by simp [oddFactors] #align odd_factors.not_two_mem oddFactors.not_two_mem -theorem oddFactors.nonneg {z a : ℤ} (ha : a ∈ oddFactors z) : 0 ≤ a := - by - simp only [oddFactors, Multiset.mem_filter] at ha - exact - Int.nonneg_of_normalize_eq_self (UniqueFactorizationMonoid.normalize_normalized_factor a ha.1) -#align odd_factors.nonneg oddFactors.nonneg - -theorem oddFactors.pow (z : ℤ) (n : ℕ) : oddFactors (z ^ n) = n • oddFactors z := +theorem oddFactors.pow (z : ℕ) (n : ℕ) : oddFactors (z ^ n) = n • oddFactors z := by simp only [oddFactors] rw [UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.filter_nsmul] #align odd_factors.pow oddFactors.pow /-- The exponent of `2` in the factorization. -/ -noncomputable def evenFactorExp (x : ℤ) := +noncomputable def evenFactorExp (x : ℕ) := Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) #align even_factor_exp evenFactorExp -theorem evenFactorExp.def (x : ℤ) : +theorem evenFactorExp.def (x : ℕ) : evenFactorExp x = Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) := rfl #align even_factor_exp.def evenFactorExp.def @@ -184,13 +155,13 @@ theorem evenFactorExp.zero : evenFactorExp 0 = 0 := rfl #align even_factor_exp.zero evenFactorExp.zero -theorem evenFactorExp.pow (z : ℤ) (n : ℕ) : evenFactorExp (z ^ n) = n * evenFactorExp z := +theorem evenFactorExp.pow (z : ℕ) (n : ℕ) : evenFactorExp (z ^ n) = n * evenFactorExp z := by simp only [evenFactorExp] rw [UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.count_nsmul] #align even_factor_exp.pow evenFactorExp.pow -theorem even_and_odd_factors'' (x : ℤ) : +theorem even_and_odd_factors'' (x : ℕ) : UniqueFactorizationMonoid.normalizedFactors x = (UniqueFactorizationMonoid.normalizedFactors x).filter (Eq 2) + oddFactors x := by @@ -205,22 +176,15 @@ theorem even_and_odd_factors'' (x : ℤ) : · symm rw [Multiset.filter_eq_self] intro a ha + rw [eq_comm] have hprime : Prime a := UniqueFactorizationMonoid.prime_of_normalized_factor a ha - have := UniqueFactorizationMonoid.normalize_normalized_factor a ha - rw [← Int.abs_eq_normalize, ← Int.coe_natAbs] at this - rw [← this] - rw [Int.prime_iff_natAbs_prime] at hprime - rcases Nat.Prime.eq_two_or_odd' hprime with (h2 | hodd) - · simp [h2] - · right - rw [this] - exact Int.natAbs_odd.1 hodd + exact hprime.nat_prime.eq_two_or_odd' · rw [Multiset.filter_eq_nil] rintro a ha ⟨rfl, hodd⟩ norm_num at hodd #align even_and_odd_factors'' even_and_odd_factors'' -theorem even_and_odd_factors' (x : ℤ) : +theorem even_and_odd_factors' (x : ℕ) : UniqueFactorizationMonoid.normalizedFactors x = Multiset.replicate (evenFactorExp x) 2 + oddFactors x := by @@ -228,7 +192,7 @@ theorem even_and_odd_factors' (x : ℤ) : simp [evenFactorExp, ← Multiset.filter_eq] #align even_and_odd_factors' even_and_odd_factors' -theorem even_and_oddFactors (x : ℤ) (hx : x ≠ 0) : +theorem even_and_oddFactors (x : ℕ) (hx : x ≠ 0) : Associated x (2 ^ evenFactorExp x * (oddFactors x).prod) := by convert(UniqueFactorizationMonoid.normalizedFactors_prod hx).symm @@ -236,74 +200,50 @@ theorem even_and_oddFactors (x : ℤ) (hx : x ≠ 0) : rw [Multiset.pow_count, ← Multiset.prod_add, ← even_and_odd_factors'' x] #align even_and_odd_factors even_and_oddFactors -theorem factors_2_even {z : ℤ} (hz : z ≠ 0) : evenFactorExp (4 * z) = 2 + evenFactorExp z := +theorem factors_2_even {z : ℕ} (hz : z ≠ 0) : evenFactorExp (4 * z) = 2 + evenFactorExp z := by - have h₀ : (4 : ℤ) ≠ 0 := four_ne_zero - have h₁ : (2 : Int) ^ 2 = 4 := by norm_num + have h₀ : (4 : ℕ) ≠ 0 := four_ne_zero + have h₁ : (2 : ℕ) ^ 2 = 4 := by norm_num simp [evenFactorExp] rw [UniqueFactorizationMonoid.normalizedFactors_mul h₀ hz, Multiset.count_add, ← h₁, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.count_nsmul, - UniqueFactorizationMonoid.normalizedFactors_irreducible Int.prime_two.irreducible, - Int.normalize_of_nonneg zero_le_two, Multiset.count_singleton_self, mul_one] + UniqueFactorizationMonoid.normalizedFactors_irreducible Nat.prime_two, + normalize_eq, Multiset.count_singleton_self, mul_one] #align factors_2_even factors_2_even -- most useful with (hz : even (even_factor_exp z)) /-- Odd factors or `4`. -/ -noncomputable def factorsOddPrimeOrFour (z : ℤ) : Multiset ℤ := +noncomputable def factorsOddPrimeOrFour (z : ℕ) : Multiset ℕ := Multiset.replicate (evenFactorExp z / 2) 4 + oddFactors z #align factors_odd_prime_or_four factorsOddPrimeOrFour -theorem factorsOddPrimeOrFour.nonneg {z a : ℤ} (ha : a ∈ factorsOddPrimeOrFour z) : 0 ≤ a := - by - simp only [factorsOddPrimeOrFour, Multiset.mem_add] at ha - cases ha with - | inl ha => - rw [Multiset.eq_of_mem_replicate ha] - norm_num - | inr ha => - exact oddFactors.nonneg ha -#align factors_odd_prime_or_four.nonneg factorsOddPrimeOrFour.nonneg - -theorem factorsOddPrimeOrFour.prod' {a : ℤ} (ha : 0 < a) (heven : Even (evenFactorExp a)) : +theorem factorsOddPrimeOrFour.prod' {a : ℕ} (ha : 0 < a) (heven : Even (evenFactorExp a)) : (factorsOddPrimeOrFour a).prod = a := by - apply Int.eq_of_associated_of_nonneg - · have := UniqueFactorizationMonoid.normalizedFactors_prod ha.ne' - apply Associated.trans _ this - obtain ⟨m, hm⟩ := even_iff_two_dvd.mp heven - rw [even_and_odd_factors' _, Multiset.prod_add, factorsOddPrimeOrFour, Multiset.prod_add, hm, - Nat.mul_div_right _ zero_lt_two, Multiset.prod_replicate, Multiset.prod_replicate, pow_mul] - exact Associated.refl _ - · apply Multiset.prod_nonneg - apply factorsOddPrimeOrFour.nonneg - · exact ha.le + have h₁ : (2 : ℕ) ^ 2 = 4 := by norm_num + have := UniqueFactorizationMonoid.normalizedFactors_prod ha.ne' + rw [associated_eq_eq] at this + conv_rhs => rw [←this] + obtain ⟨m, hm⟩ := even_iff_two_dvd.mp heven + rw [even_and_odd_factors' _, Multiset.prod_add, factorsOddPrimeOrFour, Multiset.prod_add, hm, + Nat.mul_div_right _ zero_lt_two, Multiset.prod_replicate, Multiset.prod_replicate, pow_mul, h₁] #align factors_odd_prime_or_four.prod' factorsOddPrimeOrFour.prod' -theorem factorsOddPrimeOrFour.associated' {a : ℤ} {f : Multiset ℤ} (hf : ∀ x ∈ f, OddPrimeOrFour x) - (ha : 0 < a) (heven : Even (evenFactorExp a)) (hassoc : Associated f.prod a) : - Multiset.Rel Associated f (factorsOddPrimeOrFour a) := - by - apply factors_unique_prod' hf - · intro x hx - simp only [factorsOddPrimeOrFour, Multiset.mem_add] at hx - apply Or.imp _ _ hx - · exact Multiset.eq_of_mem_replicate - · simp only [oddFactors, Multiset.mem_filter] - exact And.imp_left (UniqueFactorizationMonoid.prime_of_normalized_factor _) - · rwa [factorsOddPrimeOrFour.prod' ha heven] -#align factors_odd_prime_or_four.associated' factorsOddPrimeOrFour.associated' - -theorem factorsOddPrimeOrFour.unique' {a : ℤ} {f : Multiset ℤ} (hf : ∀ x ∈ f, OddPrimeOrFour x) - (hf' : ∀ x ∈ f, (0 : ℤ) ≤ x) (ha : 0 < a) (heven : Even (evenFactorExp a)) - (hassoc : Associated f.prod a) : f = factorsOddPrimeOrFour a := - by - rw [← Multiset.rel_eq] - apply Multiset.Rel.mono (factorsOddPrimeOrFour.associated' hf ha heven hassoc) - intro x hx y hy hxy - exact Int.eq_of_associated_of_nonneg hxy (hf' x hx) (factorsOddPrimeOrFour.nonneg hy) +theorem factorsOddPrimeOrFour.unique' {f : Multiset ℕ} (hf : ∀ x ∈ f, OddPrimeOrFour x) + (ha : 0 < f.prod) (heven : Even (evenFactorExp f.prod)) : + factorsOddPrimeOrFour f.prod = f:= + by + refine factors_unique_prod' ?_ hf (factorsOddPrimeOrFour.prod' ha heven) + intro x hx + simp only [factorsOddPrimeOrFour, Multiset.mem_add] at hx + apply Or.imp _ _ hx + · exact Multiset.eq_of_mem_replicate + · simp only [oddFactors, Multiset.mem_filter] + exact And.imp_left <| Prime.nat_prime ∘ (UniqueFactorizationMonoid.prime_of_normalized_factor _) +#align factors_odd_prime_or_four.associated' factorsOddPrimeOrFour.unique' #align factors_odd_prime_or_four.unique' factorsOddPrimeOrFour.unique' -theorem factorsOddPrimeOrFour.pow (z : ℤ) (n : ℕ) (hz : Even (evenFactorExp z)) : +theorem factorsOddPrimeOrFour.pow (z : ℕ) (n : ℕ) (hz : Even (evenFactorExp z)) : factorsOddPrimeOrFour (z ^ n) = n • factorsOddPrimeOrFour z := by simp only [factorsOddPrimeOrFour, nsmul_add, Multiset.nsmul_replicate, evenFactorExp.pow, Nat.mul_div_assoc _ (even_iff_two_dvd.mp hz), oddFactors.pow]