diff --git a/FltRegular/CaseI/AuxLemmas.lean b/FltRegular/CaseI/AuxLemmas.lean index a9d0813a..4728ea6e 100644 --- a/FltRegular/CaseI/AuxLemmas.lean +++ b/FltRegular/CaseI/AuxLemmas.lean @@ -60,7 +60,7 @@ theorem aux0k₁ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot symm intro habs rw [show (k₁ : ℤ) = 0 by simpa using habs, zero_sub] at hcong - rw [habs, _root_.pow_zero, mul_one, add_sub_cancel', aux_cong0k₁ hpri hcong] at hdiv + rw [habs, _root_.pow_zero, mul_one, add_sub_cancel_left, aux_cong0k₁ hpri hcong] at hdiv nth_rw 1 [show ζ = ζ ^ ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) by simp] at hdiv have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₁ b p j • ζ ^ j := by convert hdiv using 1 @@ -192,7 +192,6 @@ theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot rw [habs, pow_one, aux_cong1k₂ hpri hp5 hcong] at hdiv ring_nf at hdiv have key : ↑(p : ℤ) ∣ ∑ j in range p, f1k₂ a j • ζ ^ j := by - rw [Int.cast_ofNat] suffices ∑ j in range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2 by rwa [this] simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.def, ne_and_eq_iff_right diff --git a/FltRegular/CaseI/Statement.lean b/FltRegular/CaseI/Statement.lean index 0a830c9c..c39da3f4 100644 --- a/FltRegular/CaseI/Statement.lean +++ b/FltRegular/CaseI/Statement.lean @@ -92,33 +92,6 @@ theorem ab_coprime {a b c : ℤ} (H : a ^ p + b ^ p = c ^ p) (hpzero : p ≠ 0) rw [hgcd] at Hq exact hqpri.not_unit (isUnit_of_dvd_one Hq) -variable (p) - -/- -These instances are related to the problem described in -https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/slowness.20in.20ring.20theory.20file --/ - -instance foo2 : IsDedekindDomain (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)) := -inferInstance - -instance foo3 : @IsDomain (Ideal (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ))) CommSemiring.toSemiring := by - convert @Ideal.isDomain (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)) _ (foo2 p) - -noncomputable -instance foo4 : @NormalizedGCDMonoid (Ideal (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ))) - (@IsDomain.toCancelCommMonoidWithZero _ (@IdemCommSemiring.toCommSemiring _ - Submodule.instIdemCommSemiringSubmoduleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToModule) (foo3 p)) := by - convert @Ideal.instNormalizedGCDMonoidIdealToSemiringToCommSemiringCancelCommMonoidWithZero _ _ (foo2 p) - -noncomputable -instance foo5 : @GCDMonoid (Ideal (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ))) - (@IsDomain.toCancelCommMonoidWithZero _ (@IdemCommSemiring.toCommSemiring _ - Submodule.instIdemCommSemiringSubmoduleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToModule) (foo3 p)) := by - convert @NormalizedGCDMonoid.toGCDMonoid (Ideal (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ))) _ (foo4 p) - -variable {p} - theorem exists_ideal {a b c : ℤ} (h5p : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) (hgcd : ({ a, b, c } : Finset ℤ).gcd id = 1) (caseI : ¬↑p ∣ a * b * c) {ζ : R} (hζ : ζ ∈ nthRootsFinset p R) : @@ -192,7 +165,7 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime rw [natAbs_ofNat] exact emod_lt_of_pos _ (by simp [hpri.out.pos]) · simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.int_cast_eq_int_cast_iff, - ZMod.int_cast_mod, Int.cast_sub, Int.cast_mul, int_cast_ofNat, Int.cast_one] + ZMod.int_cast_mod, Int.cast_sub, Int.cast_mul, Int.cast_natCast, Int.cast_one] simp only [add_sub_assoc, sub_sub] at hk ⊢ convert hk using 3 rw [mul_add, mul_comm (↑a : R), ← mul_assoc _ (↑b : R), mul_comm _ (↑b : R), mul_assoc (↑b : R)] @@ -203,7 +176,7 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime refine' eq_of_div_eq_one _ rw [← zpow_natCast, ← zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd] simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.int_cast_zmod_eq_zero_iff_dvd, - Int.cast_sub, ZMod.int_cast_mod, Int.cast_mul, int_cast_ofNat, sub_self] + Int.cast_sub, ZMod.int_cast_mod, Int.cast_mul, Int.cast_natCast, sub_self] · rw [← Subtype.coe_inj] simp only [Fin.val_mk, SubsemiringClass.coe_pow, MulMemClass.coe_mul, NumberField.Units.coe_zpow, IsPrimitiveRoot.coe_unit'_coe, IsPrimitiveRoot.coe_inv_unit'_coe] @@ -211,7 +184,7 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime rw [← zpow_natCast, ← zpow_sub_one₀ (hζ'.ne_zero hpri.out.ne_zero), ← zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd] simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.int_cast_zmod_eq_zero_iff_dvd, - Int.cast_sub, ZMod.int_cast_mod, Int.cast_mul, int_cast_ofNat, Int.cast_one, sub_self] + Int.cast_sub, ZMod.int_cast_mod, Int.cast_mul, Int.cast_natCast, Int.cast_one, sub_self] /-- Auxiliary function -/ def f (a b : ℤ) (k₁ k₂ : ℕ) : ℕ → ℤ := fun x => diff --git a/FltRegular/FltThree/Edwards.lean b/FltRegular/FltThree/Edwards.lean index cb95ee08..6eba5935 100644 --- a/FltRegular/FltThree/Edwards.lean +++ b/FltRegular/FltThree/Edwards.lean @@ -28,7 +28,7 @@ theorem OddPrimeOrFour.im_ne_zero {p : ℤ√(-3)} (h : OddPrimeOrFour p.norm.na theorem Zsqrt3.isUnit_iff {z : ℤ√(-3)} : IsUnit z ↔ abs z.re = 1 ∧ z.im = 0 := by - rw [← Zsqrtd.norm_eq_one_iff, ← Int.coe_nat_inj', Int.ofNat_one, + rw [← Zsqrtd.norm_eq_one_iff, ← Int.natCast_inj, Int.ofNat_one, Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) z)] refine' ⟨Spts.eq_one, fun h => _⟩ rw [Zsqrtd.norm_def, h.2, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, h.1, one_pow] @@ -39,7 +39,7 @@ theorem Zsqrt3.coe_of_isUnit {z : ℤ√(-3)} (h : IsUnit z) : ∃ u : Units ℤ obtain ⟨v, hv⟩ : IsUnit z.re := by rwa [Int.isUnit_iff_abs_eq] use v rw [Zsqrtd.ext_iff, hu, ← hv] - simp only [Zsqrtd.coe_int_re, and_true_iff, eq_self_iff_true, Zsqrtd.coe_int_im] + simp only [Zsqrtd.intCast_re, and_true_iff, eq_self_iff_true, Zsqrtd.intCast_im] theorem Zsqrt3.coe_of_isUnit' {z : ℤ√(-3)} (h : IsUnit z) : ∃ u : ℤ, z = u ∧ abs u = 1 := by @@ -337,8 +337,8 @@ theorem no_conj (s : Multiset (ℤ√(-3))) {p : ℤ√(-3)} (hp : ¬IsUnit p) rw [Multiset.prod_cons, Multiset.prod_cons, ← mul_assoc, ← Zsqrtd.norm_eq_mul_conj] at hcoprime rw [Zsqrtd.isUnit_iff_norm_isUnit] apply IsCoprime.isUnit_of_dvd' hcoprime <;> - simp only [add_zero, Zsqrtd.coe_int_re, MulZeroClass.zero_mul, dvd_mul_right, Zsqrtd.mul_re, - MulZeroClass.mul_zero, Zsqrtd.mul_im, Zsqrtd.coe_int_im] + simp only [add_zero, Zsqrtd.intCast_re, MulZeroClass.zero_mul, dvd_mul_right, Zsqrtd.mul_re, + MulZeroClass.mul_zero, Zsqrtd.mul_im, Zsqrtd.intCast_im] /-- Associated elements in `ℤ√-3`. -/ def Associated' (x y : ℤ√(-3)) : Prop := @@ -438,7 +438,7 @@ theorem eq_or_eq_conj_of_associated_of_re_zero {x A : ℤ√(-3)} (hx : x.re = 0 obtain ⟨v, hv1, hv2⟩ := Zsqrt3.coe_of_isUnit' u.isUnit have hA : A.re = 0 := by simp only [← hu, hv1, hx, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_re, MulZeroClass.mul_zero, - Zsqrtd.coe_int_im] + Zsqrtd.intCast_im] rw [abs_eq <| zero_le_one' ℤ] at hv2 cases' hv2 with hv2 hv2 · left diff --git a/FltRegular/FltThree/FltThree.lean b/FltRegular/FltThree/FltThree.lean index 0acf2ec7..aeabd6b9 100644 --- a/FltRegular/FltThree/FltThree.lean +++ b/FltRegular/FltThree/FltThree.lean @@ -30,7 +30,7 @@ theorem exists_coprime {n : ℕ} (hn : 0 < n) {a b c : ℤ} (ha' : a ≠ 0) (hb' rw [← Int.pow_dvd_pow_iff hn, ← h, HA, HB, mul_pow, mul_pow, ← mul_add] exact dvd_mul_right _ _ have hdpos : 0 < d := Int.gcd_pos_of_ne_zero_left _ ha' - have hd := Int.coe_nat_ne_zero_iff_pos.mpr hdpos + have hd := Int.natCast_ne_zero_iff_pos.mpr hdpos have hsoln : A ^ n + B ^ n = C ^ n := by apply Int.eq_of_mul_eq_mul_left (pow_ne_zero n hd) @@ -227,7 +227,7 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity : have H := dvd_mul_right 2 p rw [hP] at H apply (Prime.dvd_or_dvd Int.prime_two H).resolve_left - rw [Int.coe_nat_dvd_right] + rw [Int.dvd_natCast] change ¬2 ∣ d rw [Nat.prime_dvd_prime_iff_eq Nat.prime_two hdprime] exact hne2.symm @@ -237,14 +237,14 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity : exact dvd_mul_right _ _ · have h000 : d ∣ 3 * q.natAbs ^ 2 := by - rw [← Int.coe_nat_dvd, Int.ofNat_mul, Int.coe_nat_pow, Int.natAbs_sq, Nat.cast_three] + rw [← Int.natCast_dvd_natCast, Int.ofNat_mul, Int.coe_nat_pow, Int.natAbs_sq, Nat.cast_three] use Q - d * H ^ 2 rw [mul_sub, ← hQ, hp] ring cases' (Nat.Prime.dvd_mul hdprime).mp h000 with h000 h000 · rw [Nat.prime_dvd_prime_iff_eq hdprime Nat.prime_three] at h000 exact absurd h000 hne3 - · rw [Int.coe_nat_dvd_left] + · rw [Int.natCast_dvd] exact Nat.Prime.dvd_of_dvd_pow hdprime h000 set k := g.factors.length have hg : g = 3 ^ k := by @@ -255,7 +255,7 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity : apply mul_pos zero_lt_two rwa [pos_iff_ne_zero, Int.natAbs_ne_zero] intro d hdprime hddvdg - rw [← Int.coe_nat_dvd] at hddvdg + rw [← Int.natCast_dvd_natCast] at hddvdg apply basic _ hdprime <;> apply dvd_trans hddvdg <;> rw [hg'] exacts[Int.gcd_dvd_left, Int.gcd_dvd_right] refine' ⟨k, hg, _⟩ diff --git a/FltRegular/FltThree/Spts.lean b/FltRegular/FltThree/Spts.lean index eb3a1e98..110a8c9e 100644 --- a/FltRegular/FltThree/Spts.lean +++ b/FltRegular/FltThree/Spts.lean @@ -95,8 +95,8 @@ theorem Spts.mul_of_dvd' {a p : ℤ√(-3)} (hdvd : p.norm ∣ a.norm) (hpprime rw [Zsqrtd.norm_def, HAsq] ring rw [mul_comm _ U, ← mul_assoc, ← HU, HX] - simp only [Zsqrtd.ext_iff, neg_mul, add_zero, Zsqrtd.coe_int_re, MulZeroClass.zero_mul, mul_neg, - Zsqrtd.mul_im, Zsqrtd.mul_re, neg_neg, MulZeroClass.mul_zero, neg_zero, Zsqrtd.coe_int_im, + simp only [Zsqrtd.ext_iff, neg_mul, add_zero, Zsqrtd.intCast_re, MulZeroClass.zero_mul, mul_neg, + Zsqrtd.mul_im, Zsqrtd.mul_re, neg_neg, MulZeroClass.mul_zero, neg_zero, Zsqrtd.intCast_im, this] constructor <;> ring @@ -144,7 +144,7 @@ theorem factors' (a : ℤ√(-3)) (f : ℤ) (g : ℤ) (hodd : Odd f) (hgpos : g · apply_fun abs at hfactor rw [abs_mul, h, mul_one, abs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)] at hfactor exact ⟨_, hfactor⟩ - · rw [Int.abs_eq_natAbs, ← Int.ofNat_one, Int.coe_nat_inj'] at h + · rw [Int.abs_eq_natAbs, ← Int.ofNat_one, Int.natCast_inj] at h obtain ⟨p, pprime, pdvd⟩ := Int.exists_prime_and_dvd h have : p ∣ a.norm := by rw [← hfactor] @@ -190,9 +190,9 @@ theorem Zqrtd.factor_div (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) : set c' : ℤ√(-3) := ⟨c, d⟩ refine' ⟨c', ⟨m, n⟩, _, _⟩ · - simp only [Zsqrtd.ext_iff, ha, hb, add_zero, Zsqrtd.coe_int_re, eq_self_iff_true, Zsqrtd.mul_im, + simp only [Zsqrtd.ext_iff, ha, hb, add_zero, Zsqrtd.intCast_re, eq_self_iff_true, Zsqrtd.mul_im, zero_add, Zsqrtd.add_im, and_self_iff, Zsqrtd.mul_re, MulZeroClass.mul_zero, Zsqrtd.add_re, - Zsqrtd.coe_int_im] + Zsqrtd.intCast_im] · rw [← mul_lt_mul_left (by norm_num : (0 : ℤ) < 4)] calc 4 * c'.norm = (2 * c) ^ 2 + 3 * (2 * d) ^ 2 := @@ -227,8 +227,8 @@ theorem Zqrtd.factor_div' (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) (h : 1 < |x| set e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im with he convert dvd_sub hfactor (dvd_mul_right x e) rw [he, Zsqrtd.norm_def, Zsqrtd.norm_def] - simp only [Zsqrtd.coe_int_re, Zsqrtd.mul_im, Zsqrtd.add_im, Zsqrtd.mul_re, Zsqrtd.add_re, - Zsqrtd.coe_int_im] + simp only [Zsqrtd.intCast_re, Zsqrtd.mul_im, Zsqrtd.add_im, Zsqrtd.mul_re, Zsqrtd.add_re, + Zsqrtd.intCast_im] ring refine' ⟨y, hy, _⟩ have h0'' : 0 < x.natAbs := by @@ -236,7 +236,7 @@ theorem Zqrtd.factor_div' (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) (h : 1 < |x| exact zero_lt_one.trans h rw [← mul_lt_mul_left h0'', ← pow_two, ← Int.natAbs_mul, ← hy] zify - rwa [← Int.coe_natAbs x, Int.natAbs_pow_two x, ← Int.coe_natAbs, + rwa [← Int.natCast_natAbs x, Int.natAbs_pow_two x, ← Int.natCast_natAbs, Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) c)] -- Edwards p50 step (5') @@ -285,11 +285,9 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr (hpprime.dvd_of_dvd_pow hpdvdleft)) _) (dvd_mul_of_dvd_right ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr hpdvdright) _) have := Zsqrtd.coprime_of_dvd_coprime hcoprime this - simp only [Zsqrtd.coe_int_re, isCoprime_zero_right, Zsqrtd.coe_int_im, hpprime.not_unit] at this - have h6 : x * z = C'.norm := - by - have hgnezero := Int.coe_nat_ne_zero_iff_pos.mpr hgpos - apply Int.eq_of_mul_eq_mul_left (pow_ne_zero 2 hgnezero) + simp only [Zsqrtd.intCast_re, isCoprime_zero_right, Zsqrtd.intCast_im, hpprime.not_unit] at this + have h6 : x * z = C'.norm := by + apply Int.eq_of_mul_eq_mul_left (pow_ne_zero 2 <| Int.natCast_ne_zero_iff_pos.mpr hgpos) rw [← h5, hz, mul_left_comm] have h8 : z ≠ 0 := by apply right_ne_zero_of_mul diff --git a/FltRegular/MayAssume/Lemmas.lean b/FltRegular/MayAssume/Lemmas.lean index e231633f..444525a3 100644 --- a/FltRegular/MayAssume/Lemmas.lean +++ b/FltRegular/MayAssume/Lemmas.lean @@ -61,7 +61,7 @@ theorem p_dvd_c_of_ab_of_anegc {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp : p mul_eq_zero] at h rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd] refine' Or.resolve_right h fun h3 => _ - rw [show ↑(3 : ℤ) = ((3 : ℕ) : ZMod p) by simp, ZMod.nat_cast_zmod_eq_zero_iff_dvd, + rw [show (3 : ZMod p) = ((3 : ℕ) : ZMod p) by simp, ZMod.nat_cast_zmod_eq_zero_iff_dvd, Nat.dvd_prime Nat.prime_three] at h3 cases' h3 with H₁ H₂ · exact hpri.ne_one H₁ diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean index cdfe0caf..f78ab835 100644 --- a/FltRegular/NumberTheory/AuxLemmas.lean +++ b/FltRegular/NumberTheory/AuxLemmas.lean @@ -1,6 +1,6 @@ import Mathlib.NumberTheory.RamificationInertia import Mathlib.RingTheory.Trace -import Mathlib.Data.Polynomial.Taylor +import Mathlib.Algebra.Polynomial.Taylor import Mathlib.RingTheory.Valuation.ValuationRing /-! diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean index 06d1ac2e..5b0cecb4 100644 --- a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean @@ -203,9 +203,9 @@ lemma zeta_sub_one_pow_dvd_norm_sub_pow (x : 𝓞 K) : obtain ⟨s, hs⟩ := zeta_sub_one_dvd_trace_sub_smul hζ x obtain ⟨t, ht⟩ := (associated_zeta_sub_one_pow_prime hζ).dvd rw [sub_eq_iff_eq_add] at hs - simp only [zsmul_eq_mul, Int.cast_ofNat] at hr + simp only [zsmul_eq_mul, Int.cast_natCast] at hr simp only [nsmul_eq_mul, hr, Int.cast_add, Int.cast_one, Int.cast_mul, hs, ge_iff_le, PNat.pos, - Nat.cast_pred, Int.cast_ofNat, Int.cast_pow, Nat.cast_mul, ne_eq, PNat.ne_zero, + Nat.cast_pred, Int.cast_pow, Nat.cast_mul, ne_eq, PNat.ne_zero, Int.cast_natCast, not_false_eq_true, isUnit_pow_iff] suffices (hζ.unit' - 1 : 𝓞 K) ^ (p : ℕ) ∣ (hζ.unit' - 1) * p * s + (p : 𝓞 K) ^ 2 * (r + x) by convert this using 1; ring @@ -231,9 +231,9 @@ lemma norm_add_one_smul_of_isUnit {K} [Field K] [NumberField K] {p : ℕ} (hpri intro e; apply hp obtain ⟨r, hr⟩ := Algebra.norm_one_add_smul (p : ℤ) x have : (p : ℤ) * (- Algebra.trace ℤ _ x - r * p) = 2 := by - rw [zsmul_eq_mul, Int.cast_ofNat, ← nsmul_eq_mul, e, eq_comm, ← sub_eq_zero] at hr + rw [zsmul_eq_mul, Int.cast_natCast, ← nsmul_eq_mul, e, eq_comm, ← sub_eq_zero] at hr rw [eq_comm, ← sub_eq_zero, ← hr] ring exact (Nat.prime_two.eq_one_or_self_of_dvd _ - (Int.coe_nat_dvd.mp ⟨_, this.symm⟩)).resolve_left hpri.ne_one + (Int.natCast_dvd_natCast.mp ⟨_, this.symm⟩)).resolve_left hpri.ne_one exact H.resolve_right this diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 8ddad6ea..f812886a 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -6,8 +6,7 @@ import Mathlib set_option autoImplicit false open scoped NumberField nonZeroDivisors -open FiniteDimensional -open NumberField +open FiniteDimensional NumberField variable (p : ℕ+) {K : Type*} [Field K] [NumberField K] variable {k : Type*} [Field k] [NumberField k] (hp : Nat.Prime p) @@ -251,8 +250,6 @@ lemma coe_galRestrictHom_apply (σ : K →ₐ[k] K) (x) : (galRestrictHom (𝓞 k) k K (𝓞 K) σ x : K) = σ x := algebraMap_galRestrictHom_apply (𝓞 k) k K (𝓞 K) σ x -set_option synthInstance.maxHeartbeats 160000 in -set_option maxHeartbeats 400000 in noncomputable def relativeUnitsMap (σ : K →ₐ[k] K) : RelativeUnits k K →* RelativeUnits k K := by apply QuotientGroup.lift _ @@ -467,11 +464,6 @@ lemma norm_map_inv (z : K) : Algebra.norm k z⁻¹ = (Algebra.norm k z)⁻¹ := apply eq_inv_of_mul_eq_one_left rw [← map_mul, inv_mul_cancel h, map_one] --- lemma torsion_free_lin_system [Algebra k K] (h : Monoid.IsTorsionFree (𝓞 K)ˣ) --- (ι : Fin (NumberField.Units.rank k + 1) → Additive (𝓞 k)ˣ) : --- ∃ (a : (Fin (NumberField.Units.rank k + 1) → ℤ)) (i : Fin (NumberField.Units.rank k + 1)), --- ¬ ((p : ℤ) ∣ a i) ∧ ∑ i in ⊤, (a i) • (ι i) = 0 := by sorry - lemma unitlifts_spec (S : systemOfUnits p G (NumberField.Units.rank k + 1)) (i) : mkG (Additive.toMul <| unitlifts p hp hKL σ hσ S i) = S.units i := by delta unit_to_U unitlifts @@ -502,7 +494,7 @@ theorem padicValNat_dvd_iff' {p : ℕ} (hp : p ≠ 1) (n : ℕ) (a : ℕ) : theorem padicValInt_dvd_iff' {p : ℕ} (hp : p ≠ 1) (n : ℕ) (a : ℤ) : (p : ℤ) ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a := by - rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff' hp, ← Int.coe_nat_dvd_left, + rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff' hp, ← Int.natCast_dvd, Int.coe_nat_pow] theorem padicValInt_dvd' {p : ℕ} (a : ℤ) : (p : ℤ) ^ padicValInt p a ∣ a := by @@ -591,13 +583,13 @@ lemma lh_pow_free' {M} [CommGroup M] [Module.Finite ℤ (Additive M)] (ζ : M) refine ⟨α₂ - α₁, β₁ • Function.extend Fin.castSucc ι₁ 0 - β₂ • Function.extend (Fin.succAbove i₁.castSucc) ι₂ 0, i₁.castSucc, ?_, ?_, fun H ↦ (hζ' H).elim⟩ · rw [sub_mul, eq_sub_iff_add_eq.mpr h₁, eq_sub_iff_add_eq.mpr h₂] - simp only [zsmul_eq_mul, Pi.coe_int, Int.cast_id, Pi.sub_apply, Pi.mul_apply, + simp only [zsmul_eq_mul, Pi.intCast_def, Int.cast_id, Pi.sub_apply, Pi.mul_apply, Fin.succAbove_of_le_castSucc, ne_eq, not_not, not_exists, sub_sub_sub_cancel_left] simp only [sub_smul, mul_smul, ← e₁, ← e₂, sum_sub_distrib] rw [Fin.sum_univ_castSucc, Fin.sum_univ_succAbove _ i₁.castSucc] simp [(Fin.castSucc_injective r).extend_apply, Fin.succAbove_right_injective.extend_apply, (Fin.castSucc_lt_last _).ne, smul_sum] - · simp only [zsmul_eq_mul, Pi.coe_int, Int.cast_id, Pi.sub_apply, Pi.mul_apply, + · simp only [zsmul_eq_mul, Pi.intCast_def, Int.cast_id, Pi.sub_apply, Pi.mul_apply, exists_apply_eq_apply, not_true_eq_false, (Fin.castSucc_injective r).extend_apply, Fin.exists_succAbove_eq_iff, ne_eq, not_false_eq_true, Function.extend_apply', Pi.zero_apply, mul_zero, sub_zero, (Nat.prime_iff_prime_int.mp hp).dvd_mul, hi₁, not_or, and_true] @@ -623,22 +615,6 @@ lemma lh_pow_free [Algebra k K] [IsGalois k K] [FiniteDimensional k K] (ζ : ( · rw [NumberField.Units.finrank_eq] exact Nat.lt.base _ --- lemma IsPrimitiveRoot.totient_le_finrank {R} [CommRing R] [IsDomain R] [CharZero R] --- [Module.Finite ℤ R] {ζ : R} {r} --- (hζ : IsPrimitiveRoot ζ r) : r.totient ≤ finrank ℤ R := by --- by_cases hr : r = 0 --- · rw [hr]; exact Nat.zero_le _ --- replace hr := Nat.pos_iff_ne_zero.mpr hr --- calc --- _ ≤ (minpoly ℤ ζ).natDegree := --- hζ.totient_le_degree_minpoly --- _ = (Algebra.adjoin.powerBasis' (hζ.isIntegral hr)).dim := --- (Algebra.adjoin.powerBasis'_dim (hζ.isIntegral hr)).symm --- _ = finrank ℤ ↥(Algebra.adjoin ℤ {ζ}) := --- (Algebra.adjoin.powerBasis' (hζ.isIntegral hr)).finrank'.symm --- _ ≤ finrank ℤ R := --- Submodule.finrank_le (Subalgebra.toSubmodule (Algebra.adjoin ℤ {ζ})) - lemma Subgroup.isCyclic_of_le {M : Type*} [Group M] {H₁ H₂ : Subgroup M} [IsCyclic H₂] (e : H₁ ≤ H₂) : IsCyclic H₁ := isCyclic_of_surjective _ (subgroupOfEquivOfLe e).surjective @@ -674,27 +650,6 @@ lemma norm_map_zpow {R S} [Field R] [DivisionRing S] [Nontrivial S] [Algebra R S [Module.Free R S] [Module.Finite R S] (s : S) (n : ℤ) : Algebra.norm R (s ^ n) = (Algebra.norm R s) ^ n := map_zpow₀ (Algebra.normZeroHom R S) s n --- lemma h_exists : ∃ (h : ℕ) (ζ : (𝓞 k)ˣ), --- IsPrimitiveRoot (ζ : k) (p ^ h) ∧ ∀ ε : k, ¬ IsPrimitiveRoot ε (p ^ (h + 1)) := by --- classical --- have H : ∃ n, ∀ ε : k, ¬ IsPrimitiveRoot ε (p ^ n : ℕ+) --- · use finrank ℤ (𝓞 k) + 1 --- intro ζ hζ --- have := hζ.unit'_coe.totient_le_finrank --- generalize finrank ℤ (𝓞 k) = n at this --- rw [PNat.pow_coe, Nat.totient_prime_pow_succ hp] at this --- have := (Nat.mul_le_mul_left _ (show (1 : ℕ) ≤ ↑p - 1 from --- le_tsub_of_add_le_right hp.two_le)).trans_lt (this.trans_lt n.lt_two_pow) --- simp only [mul_one] at this --- exact (lt_of_pow_lt_pow _ (Nat.zero_le _) this).not_le hp.two_le --- cases h : Nat.find H with --- | zero => simp at h --- | succ n => --- have := Nat.find_min H ((Nat.lt_succ.mpr le_rfl).trans_le h.ge) --- simp only [not_forall, not_not] at this --- obtain ⟨ζ, hζ⟩ := this --- refine ⟨n, hζ.unit', hζ, by simpa only [h] using Nat.find_spec H⟩ - local notation "r" => NumberField.Units.rank k lemma Units.coe_val_inv {M S} [DivisionMonoid M] @@ -718,9 +673,6 @@ lemma norm_eq_prod_pow_gen rw [Finset.prod_set_coe (α := K ≃ₐ[k] K) (β := K) (f := fun i ↦ i η) (Subgroup.zpowers σ)] congr; ext; simp [hσ] -attribute [-instance] instCoeOut - -set_option synthInstance.maxHeartbeats 160000 in lemma Hilbert92ish_aux0 (h : ℕ) (ζ : (𝓞 k)ˣ) (hζ : IsPrimitiveRoot (ζ : k) (p ^ h)) (H : ∀ ε : (𝓞 K)ˣ, algebraMap k K ζ ^ ((p : ℕ) ^ (h - 1)) ≠ ε / (σ ε : K)) : ∃ η : (𝓞 K)ˣ, Algebra.norm k (η : K) = 1 ∧ ∀ ε : (𝓞 K)ˣ, (η : K) ≠ ε / (σ ε : K) := by @@ -742,7 +694,6 @@ lemma Hilbert92ish_aux0 (h : ℕ) (ζ : (𝓞 k)ˣ) (hζ : IsPrimitiveRoot (ζ : SubmonoidClass.coe_pow] rfl -set_option synthInstance.maxHeartbeats 160000 in lemma Hilbert92ish_aux1 (n : ℕ) (H : Fin n → Additive (𝓞 K)ˣ) (ζ : (𝓞 k)ˣ) (a : ℤ) (ι : Fin n → ℤ) (η : Fin n → Additive (𝓞 k)ˣ) (ha : ∑ i : Fin n, ι i • η i = (a * ↑↑p) • Additive.ofMul ζ) diff --git a/FltRegular/NumberTheory/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean index 58d61035..ac8d37e9 100644 --- a/FltRegular/NumberTheory/KummersLemma/Field.lean +++ b/FltRegular/NumberTheory/KummersLemma/Field.lean @@ -3,7 +3,6 @@ import Mathlib.NumberTheory.Cyclotomic.Rat import Mathlib.FieldTheory.KummerExtension import FltRegular.NumberTheory.Unramified import FltRegular.NumberTheory.Cyclotomic.MoreLemmas -import Mathlib.Data.Polynomial.Taylor open scoped NumberField BigOperators @@ -142,7 +141,7 @@ theorem roots_poly {L : Type*} [Field L] [Algebra K L] (α : L) simp only [Finset.image_val, Finset.range_val, Multiset.mem_dedup, Multiset.mem_map, Multiset.mem_range] at hx obtain ⟨m, _, rfl⟩ := hx - rw [mem_roots, IsRoot.definition, eval_map, ← aeval_def, aeval_poly hp hζ u hcong α e] + rw [mem_roots, IsRoot.def, eval_map, ← aeval_def, aeval_poly hp hζ u hcong α e] exact ((monic_poly hp hζ u hcong).map (algebraMap (𝓞 K) L)).ne_zero · intros i hi j hj e apply (hζ.map_of_injective (algebraMap K L).injective).injOn_pow_mul hα hi hj diff --git a/FltRegular/ReadyForMathlib/Homogenization.lean b/FltRegular/ReadyForMathlib/Homogenization.lean index eafb0336..78ae6673 100644 --- a/FltRegular/ReadyForMathlib/Homogenization.lean +++ b/FltRegular/ReadyForMathlib/Homogenization.lean @@ -5,7 +5,6 @@ Authors: Alex J. Best ! This file was ported from Lean 3 source module ready_for_mathlib.homogenization -/ -import Mathlib.Data.MvPolynomial.CommRing import Mathlib.Data.Set.Finite import Mathlib.RingTheory.MvPolynomial.Homogeneous import Mathlib.RingTheory.Polynomial.Basic diff --git a/lake-manifest.json b/lake-manifest.json index e4aba471..e46d6ac9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "67c40f89be2c17c6f4b0b6056d2de8591c0f92d3", + "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "fd760831487e6835944e7eeed505522c9dd47563", + "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "8be30c25e3caa06937feeb62f7ca898370f80ee9", + "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "1cca755bf20cfcec06dc01cdf4efac4e80b635eb", + "rev": "029ba7606b2856f16ad0b3324f9ec786cf11ec0c", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index e35881ce..9ad30404 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0-rc2 +leanprover/lean4:v4.7.0