bump

Author: riccardobrasca

FltRegular.lean

@@ -9,7 +9,6 @@ import FltRegular.MayAssume.Lemmas
 import FltRegular.NumberTheory.Cyclotomic.CaseI
 import FltRegular.NumberTheory.Cyclotomic.CyclRat
 import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits
-import FltRegular.NumberTheory.Cyclotomic.Factoring
 import FltRegular.NumberTheory.Cyclotomic.GaloisActionOnCyclo
 import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas

FltRegular/CaseI/Statement.lean

@@ -1,5 +1,4 @@
 import FltRegular.MayAssume.Lemmas
-import FltRegular.NumberTheory.Cyclotomic.Factoring
 import FltRegular.NumberTheory.Cyclotomic.CaseI
 import FltRegular.CaseI.AuxLemmas
 import FltRegular.NumberTheory.RegularPrimes
@@ -140,8 +139,8 @@ theorem exists_ideal {a b c : ℤ} (h5p : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p)
   have H₁ := congr_arg (algebraMap ℤ R) H
   simp only [eq_intCast, Int.cast_add, Int.cast_pow] at H₁
   have hζ' := (zeta_spec P ℚ K).unit'_coe
-  rw [pow_add_pow_eq_prod_add_zeta_runity_mul _ _
-    (hpri.out.eq_two_or_odd.resolve_left fun h => by simp [h] at h5p) hζ'] at H₁
+  rw [hζ'.pow_add_pow_eq_prod_add_mul _ _ <|
+    odd_iff.2 <| hpri.1.eq_two_or_odd.resolve_left fun h ↦ by simp [h] at h5p] at H₁
   replace H₁ := congr_arg (fun x => span ({ x } : Set R)) H₁
   simp only [← prod_span_singleton, ← span_singleton_pow] at H₁
   refine exists_eq_pow_of_mul_eq_pow_of_coprime (fun η₁ hη₁ η₂ hη₂ hη => ?_) H₁ ζ hζ

FltRegular/CaseII/InductionStep.lean

@@ -1,6 +1,5 @@
 import FltRegular.CaseII.AuxLemmas
 import FltRegular.NumberTheory.KummersLemma.KummersLemma
-import FltRegular.NumberTheory.Cyclotomic.Factoring
 
 open scoped BigOperators nonZeroDivisors NumberField
 open Polynomial
@@ -70,8 +69,8 @@ include hp hζ e hz in
 lemma x_plus_y_mul_ne_zero : x + y * η ≠ 0 := by
   intro hη
   have : x + y * η ∣ x ^ (p : ℕ) + y ^ (p : ℕ) := by
-    rw [pow_add_pow_eq_prod_add_zeta_runity_mul _ _
-      (hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)) hζ.unit'_coe]
+    rw [hζ.unit'_coe.pow_add_pow_eq_prod_add_mul _ _ <| Nat.odd_iff.2 <|
+      hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)]
     simp_rw [mul_comm _ y]
     exact Finset.dvd_prod_of_mem _ η.prop
   rw [hη, zero_dvd_iff, e] at this
@@ -90,8 +89,9 @@ lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
   letI := IsCyclotomicExtension.numberField {p} ℚ K
   have h := zeta_sub_one_dvd hζ e
   replace h : ∏ _η in nthRootsFinset p (𝓞 K), Ideal.Quotient.mk 𝔭 (x + y * η : 𝓞 K) = 0 := by
-    rw [pow_add_pow_eq_prod_add_zeta_runity_mul _ _ (hpri.out.eq_two_or_odd.resolve_left
-      (PNat.coe_injective.ne hp)) hζ.unit'_coe, ← Ideal.Quotient.eq_zero_iff_dvd, map_prod] at h
+    rw [hζ.unit'_coe.pow_add_pow_eq_prod_add_mul _ _ <| Nat.odd_iff.2 <|
+      hpri.out.eq_two_or_odd.resolve_left
+      (PNat.coe_injective.ne hp), ← Ideal.Quotient.eq_zero_iff_dvd, map_prod] at h
     convert h using 2 with η' hη'
     rw [map_add, map_add, map_mul, map_mul, IsPrimitiveRoot.eq_one_mod_one_sub' hζ.unit'_coe hη',
       IsPrimitiveRoot.eq_one_mod_one_sub' hζ.unit'_coe η.prop, one_mul, mul_one]
@@ -249,8 +249,8 @@ lemma exists_ideal_pow_eq_c_aux :
 /- The ∏_η,  𝔠 η = (𝔷' 𝔭^m)^p with 𝔷 = 𝔪 𝔷' -/
 lemma prod_c : ∏ η in Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = (𝔷' * 𝔭 ^ m) ^ (p : ℕ) := by
   have e' := span_pow_add_pow_eq hζ e
-  rw [pow_add_pow_eq_prod_add_zeta_runity_mul _ _
-    (hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)) hζ.unit'_coe] at e'
+  rw [hζ.unit'_coe.pow_add_pow_eq_prod_add_mul _ _ <| Nat.odd_iff.2 <|
+    hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)] at e'
   rw [← Ideal.prod_span_singleton, ← Finset.prod_attach] at e'
   simp_rw [mul_comm _ y, ← m_mul_c_mul_p hp hζ e hy,
     Finset.prod_mul_distrib, Finset.prod_const, Finset.card_attach,

FltRegular/NumberTheory/Cyclotomic/Factoring.lean

@@ -341,8 +341,9 @@ lemma isTors' [IsGalois k K] : Module.IsTorsionBySet ℤ[X]
   simp only [Units.coe_map, MonoidHom.coe_coe, RingOfIntegers.coe_algebraMap_norm, map_pow,
     Units.coe_prod, Submonoid.coe_finset_prod, Subsemiring.coe_toSubmonoid,
     Subalgebra.coe_toSubsemiring, Algebra.norm_eq_prod_automorphisms]
-  rw [← hKL, ← IsGalois.card_aut_eq_finrank, ← orderOf_eq_card_of_forall_mem_zpowers hσ,
-    ← Fin.prod_univ_eq_prod_range, ← (finEquivZPowers σ <| isOfFinOrder_of_finite _).symm.prod_comp]
+  rw [← hKL, ← IsGalois.card_aut_eq_finrank, Fintype.card_eq_nat_card,
+    ← orderOf_eq_card_of_forall_mem_zpowers hσ, ← Fin.prod_univ_eq_prod_range,
+    ← (finEquivZPowers σ <| isOfFinOrder_of_finite _).symm.prod_comp]
   simp only [pow_finEquivZPowers_symm_apply, coe_galRestrictHom_apply, AlgHom.coe_coe, map_prod]
   rw [Finset.prod_set_coe (α := K ≃ₐ[k] K) (β := K) (f := fun i ↦ i ↑x) (Subgroup.zpowers σ)]
   congr
@@ -660,7 +661,7 @@ lemma Hilbert92_aux2 (E : (𝓞 K)ˣ) (ν : k) (hE : algebraMap k K ν = E / σ
       rw [hE]
       field_simp
   rw [norm_eq_prod_pow_gen σ hσ, orderOf_eq_card_of_forall_mem_zpowers hσ,
-    IsGalois.card_aut_eq_finrank, hKL]
+    ← Fintype.card_eq_nat_card, IsGalois.card_aut_eq_finrank, hKL]
   conv =>
     enter [1, 2, i]
     rw [h1 i, mul_comm]

FltRegular/NumberTheory/Hilbert92.lean

@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6d297a4172e6c37d3bf82e68924c45d72621ac5d",
+   "rev": "2c6450e45a0b2b45662a8289c3d0fbf09883939f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,