wip

FltRegular/FltThree/FltThree.lean

@@ -686,7 +686,7 @@ theorem descent (a b c : ℤ) (h : FltCoprime 3 a b c) :
     by
     obtain ⟨a', b', c', ha', hb', hc', hsmaller, hsolution⟩ := this
     refine' ⟨a', b', c', ha', hb', hc', _, hsolution⟩
-    rw [← Nat.pow_lt_iff_lt_left (by norm_num : 1 ≤ 3)]
+    rw [← Nat.pow_lt_pow_iff_left three_ne_zero]
     convert lt_of_le_of_lt hsmaller haaa <;> simp [mul_pow, Int.natAbs_mul, Int.natAbs_pow]
   -- 4.
   cases' gcd1or3 p q hp hcoprime hodd with hgcd hgcd

FltRegular/FltThree/Primes.lean

@@ -46,8 +46,7 @@ theorem Int.factor_div (a x : ℤ) (hodd : Odd x) :
       exact ⟨_, heqtwomul⟩
 
 theorem two_not_cube (r : ℕ) : r ^ 3 ≠ 2 :=by
-  have : 1 ≤ 3 := by norm_num
-  apply Monotone.ne_of_lt_of_lt_nat (Nat.pow_left_strictMono this).monotone 1 <;> norm_num
+  apply Monotone.ne_of_lt_of_lt_nat (Nat.pow_left_strictMono three_ne_zero).monotone 1 <;> norm_num
 
 namespace Mathlib
 open Lean hiding Rat mkRat

FltRegular/FltThree/Spts.lean

@@ -204,11 +204,11 @@ theorem Zqrtd.factor_div (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) :
 
     · rw [mul_pow, ← Int.natAbs_pow_two c, ← Int.natAbs_pow_two x, ← mul_pow]
       norm_cast
-      exact Nat.pow_lt_pow_of_lt_left hc zero_lt_two
+      exact Nat.pow_lt_pow_left hc two_ne_zero
     · rw [mul_pow, ← Int.natAbs_pow_two d, ← Int.natAbs_pow_two x, ← mul_pow,
         mul_lt_mul_left (by norm_num : (0 : ℤ) < 3)]
       norm_cast
-      exact Nat.pow_lt_pow_of_lt_left hd zero_lt_two
+      exact Nat.pow_lt_pow_left hd two_ne_zero
 
 theorem Zqrtd.factor_div' (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) (h : 1 < |x|)
     (hcoprime : IsCoprime a.re a.im) (hfactor : x ∣ a.norm) :
@@ -326,13 +326,13 @@ theorem Spts.eq_one {a : ℤ√(-3)} (h : a.norm = 1) : abs a.re = 1 ∧ a.im =
     · have : 1 ≤ abs a.im := by rwa [← Int.abs_lt_one_iff, not_lt] at hb
       have : 1 ≤ a.im ^ 2 := by
         rw [← sq_abs]
-        exact pow_le_pow_of_le_left zero_le_one this 2
+        exact pow_le_pow_left zero_le_one this 2
       linarith
   · apply ne_of_gt
     rw [Zsqrtd.norm_def, neg_mul, neg_mul, sub_neg_eq_add]
     apply lt_add_of_lt_of_nonneg
     · rw [← sq, ← sq_abs]
-      exact pow_lt_pow_of_lt_left H zero_le_one zero_lt_two
+      exact pow_lt_pow_left H zero_le_one two_ne_zero
     · rw [mul_assoc]
       exact mul_nonneg zero_lt_three.le (mul_self_nonneg _)
 
@@ -371,7 +371,7 @@ theorem Spts.not_two (a : ℤ√(-3)) : a.norm ≠ 2 :=
   obtain him | him := eq_or_ne a.im 0
   · rw [him, MulZeroClass.mul_zero, sub_zero, ← Int.natAbs_mul_self, ← sq]
     norm_cast
-    apply (Nat.pow_left_strictMono one_le_two).monotone.ne_of_lt_of_lt_nat 1 <;> norm_num
+    apply (Nat.pow_left_strictMono two_ne_zero).monotone.ne_of_lt_of_lt_nat 1 <;> norm_num
   · apply ne_of_gt
     apply lt_add_of_nonneg_of_lt (mul_self_nonneg a.re)
     rw [← Int.add_one_le_iff]

FltRegular/NumberTheory/AuxLemmas.lean

@@ -567,27 +567,6 @@ theorem span_range_natDegree_eq_adjoin {R A} [CommRing R] [CommRing A] [Algebra
   rw [Finset.mem_range]
   exact (le_natDegree_of_mem_supp _ hkq).trans_lt this
 
--- Mathlib/Data/Polynomial/RingDivision.lean
-open Polynomial BigOperators in
-lemma Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero {R} [CommRing R] [IsDomain R]
-    (p : R[X]) {ι} [Fintype ι] {f : ι → R} (hf : Function.Injective f)
-    (heval : ∀ i, p.eval (f i) = 0) (hcard : natDegree p < Fintype.card ι) : p = 0 := by
-  classical
-  by_contra hp
-  apply not_lt_of_le (le_refl (Finset.card p.roots.toFinset))
-  calc
-    Finset.card p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
-    _ ≤ natDegree p := Polynomial.card_roots' p
-    _ < Fintype.card ι := hcard
-    _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
-    _ = Finset.card (Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
-    _ ≤ Finset.card p.roots.toFinset := Finset.card_mono ?_
-  intro _
-  simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
-    IsRoot.def, forall_exists_index, hp, not_false_eq_true]
-  rintro x rfl
-  exact heval _
-
 -- Dunno. Somewhere near Mathlib/FieldTheory/Minpoly/Basic.lean.
 lemma aeval_derivative_minpoly_ne_zero {K L} [CommRing K] [CommRing L] [Algebra K L] (x : L)
     (hx : (minpoly K x).Separable) [Nontrivial L] :

FltRegular/NumberTheory/CyclotomicRing.lean

@@ -30,11 +30,6 @@ def AdjoinRoot.equivOfMinpolyEq {R S} [CommRing R] [CommRing S] [Algebra R S]
     (P : R[X]) (pb : PowerBasis R S) (hpb : minpoly R pb.gen = P) :
     AdjoinRoot P ≃ₐ[R] S := AdjoinRoot.equiv' P pb (hpb ▸ aeval_root _) (hpb ▸ minpoly.aeval _ _)
 
-theorem map_dvd_iff {M N} [Monoid M] [Monoid N] {F : Type*} [MulEquivClass F M N] (f : F) {a b} :
-    f a ∣ f b ↔ a ∣ b := by
-  refine ⟨?_, map_dvd f⟩
-  convert _root_.map_dvd (f : M ≃* N).symm <;> exact ((f : M ≃* N).symm_apply_apply _).symm
-
 namespace CyclotomicIntegers
 
 @[simps! (config := .lemmasOnly)]

FltRegular/NumberTheory/Different.lean

@@ -1,7 +1,7 @@
+import Mathlib.RingTheory.DedekindDomain.Different
 import Mathlib.RingTheory.DedekindDomain.Ideal
 import Mathlib.RingTheory.Discriminant
 import Mathlib.RingTheory.Localization.FractionRing
-import FltRegular.NumberTheory.MinpolyDiv
 import FltRegular.NumberTheory.QuotientTrace
 import Mathlib.NumberTheory.KummerDedekind
 /-!
@@ -134,7 +134,8 @@ lemma isIntegral_discr_mul_of_mem_traceFormDualSubmodule
 
 variable (A K)
 
-def FractionalIdeal.dual (I : FractionalIdeal B⁰ L) (hI : I ≠ 0) :
+-- TODO: merge with FractionalIdeal.dual
+def FractionalIdeal.dual₂ (I : FractionalIdeal B⁰ L) (hI : I ≠ 0) :
     FractionalIdeal B⁰ L :=
   ⟨traceFormDualSubmodule A K I, by
     classical
@@ -155,13 +156,13 @@ def FractionalIdeal.dual (I : FractionalIdeal B⁰ L) (hI : I ≠ 0) :
 
 variable {A K}
 
-lemma FractionalIdeal.mem_dual {I : FractionalIdeal B⁰ L} {hI : I ≠ 0} {x} :
-  x ∈ dual A K I hI ↔ ∀ a ∈ I, Algebra.traceForm K L x a ∈ (algebraMap A K).range := Iff.rfl
+lemma FractionalIdeal.mem_dual₂ {I : FractionalIdeal B⁰ L} {hI : I ≠ 0} {x} :
+  x ∈ dual₂ A K I hI ↔ ∀ a ∈ I, Algebra.traceForm K L x a ∈ (algebraMap A K).range := Iff.rfl
 
-lemma FractionalIdeal.dual_ne_zero {I : FractionalIdeal B⁰ L} {hI : I ≠ 0} :
-    dual A K I hI ≠ 0 := by
+lemma FractionalIdeal.dual₂_ne_zero {I : FractionalIdeal B⁰ L} {hI : I ≠ 0} :
+    dual₂ A K I hI ≠ 0 := by
   obtain ⟨b, hb, hb'⟩ := I.prop
-  suffices algebraMap B L b ∈ dual A K I hI by
+  suffices algebraMap B L b ∈ dual₂ A K I hI by
     intro e
     rw [e, mem_zero_iff, ← (algebraMap B L).map_zero,
       (IsIntegralClosure.algebraMap_injective B A L).eq_iff] at this
@@ -175,8 +176,8 @@ lemma FractionalIdeal.dual_ne_zero {I : FractionalIdeal B⁰ L} {hI : I ≠ 0} :
     exact IsIntegralClosure.isIntegral_iff (A := B)
   · exact (Algebra.smul_def _ _).symm
 
-lemma FractionalIdeal.le_dual_inv_aux (I J: FractionalIdeal B⁰ L) (hI) (hIJ : I * J ≤ 1) :
-    J ≤ dual A K I hI := by
+lemma FractionalIdeal.le_dual₂_inv_aux (I J: FractionalIdeal B⁰ L) (hI) (hIJ : I * J ≤ 1) :
+    J ≤ dual₂ A K I hI := by
   intro x hx y hy
   apply IsIntegrallyClosed.isIntegral_iff.mp
   apply isIntegral_trace
@@ -189,16 +190,16 @@ variable [IsDedekindDomain B] [IsFractionRing B L]
 
 variable (A K)
 
-lemma FractionalIdeal.inv_le_dual (I : FractionalIdeal B⁰ L) (hI) :
-    I⁻¹ ≤ dual A K I hI :=
-  le_dual_inv_aux _ _ _ (le_of_eq (mul_inv_cancel hI))
+lemma FractionalIdeal.inv_le_dual₂ (I : FractionalIdeal B⁰ L) (hI) :
+    I⁻¹ ≤ dual₂ A K I hI :=
+  le_dual₂_inv_aux _ _ _ (le_of_eq (mul_inv_cancel hI))
 
-lemma FractionalIdeal.dual_inv_le (I : FractionalIdeal B⁰ L) (hI) :
-    (dual A K I hI)⁻¹ ≤ I := by
-  convert mul_right_mono ((dual A K I hI)⁻¹)
-    (mul_left_mono I (FractionalIdeal.inv_le_dual A K I hI)) using 1
+lemma FractionalIdeal.dual₂_inv_le (I : FractionalIdeal B⁰ L) (hI) :
+    (dual₂ A K I hI)⁻¹ ≤ I := by
+  convert mul_right_mono ((dual₂ A K I hI)⁻¹)
+    (mul_left_mono I (FractionalIdeal.inv_le_dual₂ A K I hI)) using 1
   · simp only [mul_inv_cancel hI, one_mul]
-  · simp only [mul_inv_cancel (FractionalIdeal.dual_ne_zero (hI := hI)), mul_assoc, mul_one]
+  · simp only [mul_inv_cancel (FractionalIdeal.dual₂_ne_zero (hI := hI)), mul_assoc, mul_one]
 
 variable (B)
 
@@ -214,12 +215,12 @@ lemma coeSubmodule_differentIdeal' [NoZeroSMulDivisors A B] (hAB : Algebra.IsInt
   have : IsIntegralClosure B A (FractionRing B) :=
     isIntegralClosure_of_isIntegrallyClosed _ _ _ hAB
   rw [coeSubmodule, differentIdeal, Submodule.map_comap_eq, inf_eq_right]
-  have := FractionalIdeal.dual_inv_le A (FractionRing A) (1 : FractionalIdeal B⁰ (FractionRing B))
+  have := FractionalIdeal.dual₂_inv_le A (FractionRing A) (1 : FractionalIdeal B⁰ (FractionRing B))
     one_ne_zero
   have : _ ≤ ((1 : FractionalIdeal B⁰ (FractionRing B)) : Submodule B (FractionRing B)) := this
   simp only [← one_div, FractionalIdeal.val_eq_coe,
-    FractionalIdeal.coe_div FractionalIdeal.dual_ne_zero] at this
-  dsimp [FractionalIdeal.dual] at this
+    FractionalIdeal.coe_div FractionalIdeal.dual₂_ne_zero] at this
+  dsimp [FractionalIdeal.dual₂] at this
   simpa only [FractionalIdeal.coe_one] using this
 
 lemma coeSubmodule_differentIdeal [NoZeroSMulDivisors A B] :
@@ -251,17 +252,17 @@ variable (L)
 
 lemma coeIdeal_different_ideal [NoZeroSMulDivisors A B] :
     ↑(differentIdeal A B) =
-      (FractionalIdeal.dual A K (1 : FractionalIdeal B⁰ L) one_ne_zero)⁻¹ := by
+      (FractionalIdeal.dual₂ A K (1 : FractionalIdeal B⁰ L) one_ne_zero)⁻¹ := by
   apply FractionalIdeal.coeToSubmodule_injective
-  simp only [FractionalIdeal.coe_div FractionalIdeal.dual_ne_zero,
+  simp only [FractionalIdeal.coe_div FractionalIdeal.dual₂_ne_zero,
     FractionalIdeal.coe_coeIdeal, coeSubmodule_differentIdeal A K, inv_eq_one_div]
-  simp only [FractionalIdeal.dual, FractionalIdeal.coe_mk, FractionalIdeal.coe_one]
+  simp only [FractionalIdeal.dual₂, FractionalIdeal.coe_mk, FractionalIdeal.coe_one]
 
 lemma differentialIdeal_le_fractionalIdeal_iff
   (I : FractionalIdeal B⁰ L) (hI : I ≠ 0) [NoZeroSMulDivisors A B] :
     differentIdeal A B ≤ I ↔ (((I⁻¹ : _) : Submodule B L).restrictScalars A).map
       ((Algebra.trace K L).restrictScalars A) ≤ 1 := by
-  rw [coeIdeal_different_ideal A K B L, FractionalIdeal.inv_le_comm FractionalIdeal.dual_ne_zero hI]
+  rw [coeIdeal_different_ideal A K B L, FractionalIdeal.inv_le_comm FractionalIdeal.dual₂_ne_zero hI]
   refine le_traceFormDualSubmodule.trans ?_
   simp
 
@@ -415,7 +416,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B]
   apply FractionalIdeal.coeIdeal_injective (K := L)
   simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton]
   rw [coeIdeal_different_ideal A K B L,
-    mul_inv_eq_iff_eq_mul₀ FractionalIdeal.dual_ne_zero]
+    mul_inv_eq_iff_eq_mul₀ FractionalIdeal.dual₂_ne_zero]
   apply FractionalIdeal.coeToSubmodule_injective
   simp only [FractionalIdeal.coe_coeIdeal, FractionalIdeal.coe_mul,
     FractionalIdeal.coe_spanSingleton, Submodule.span_singleton_mul]
@@ -425,7 +426,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B]
   have : algebraMap B L (aeval x (derivative (minpoly A x))) ≠ 0
   · rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map,
       aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁
-  rw [Submodule.mem_smul_iff_inv this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual,
+  rw [Submodule.mem_smul_iff_inv this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual₂,
     mem_coeIdeal_conductor]
   have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0
   · rwa [ne_eq, inv_eq_zero]

FltRegular/NumberTheory/Hilbert90.lean

@@ -17,12 +17,12 @@ noncomputable
 def ηu : Lˣ := (Ne.isUnit (fun h ↦ by simp [h] at hη) : IsUnit η).unit
 
 noncomputable
-def φ := (finEquivZpowers _ (isOfFinOrder_of_finite σ)).symm
+def φ := (finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm
 
 variable {σ}
 
 lemma hφ : ∀ (n : ℕ), φ σ ⟨σ ^ n, hσ _⟩ = n % (orderOf σ) := fun n ↦ by
-  simpa [Fin.ext_iff] using finEquivZpowers_symm_apply _ (isOfFinOrder_of_finite σ) n
+  simpa [Fin.ext_iff] using finEquivZPowers_symm_apply _ (isOfFinOrder_of_finite σ) n
 
 noncomputable
 def cocycle : (L ≃ₐ[K] L) → Lˣ := fun τ ↦ ∏ i in range (φ σ ⟨τ, hσ τ⟩), Units.map (σ ^ i) (ηu hη)
@@ -45,8 +45,8 @@ lemma foo {a: ℕ} (h : a % orderOf σ = 0) :
       (fun a b ha hb hab ↦ ?_) (fun τ _ ↦ ?_)
     · rwa [pow_inj_mod, Nat.mod_eq_of_lt (Finset.mem_range.1 ha),
         Nat.mod_eq_of_lt (Finset.mem_range.1 hb)] at hab
-    · refine ⟨(finEquivZpowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩, by simp, ?_⟩
-      have := Equiv.symm_apply_apply (finEquivZpowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩
+    · refine ⟨(finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩, by simp, ?_⟩
+      have := Equiv.symm_apply_apply (finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩
       simp only [SetLike.coe_sort_coe, Equiv.symm_symm, ← Subtype.coe_inj] at this ⊢
       rw [← this]
       simp only [SetLike.coe_sort_coe, Subtype.coe_eta, Equiv.symm_apply_apply]

FltRegular/NumberTheory/Hilbert92.lean

@@ -301,9 +301,10 @@ def Group.forall_mem_zpowers_iff {H} [Group H] {x : H} :
   rw [SetLike.ext_iff]
   simp only [Subgroup.mem_top, iff_true]
 
-lemma pow_finEquivZpowers_symm_apply {M} [Group M] (x : M) (hx) (a) :
-    x ^ ((finEquivZpowers x hx).symm a : ℕ) = a :=
-  congr_arg Subtype.val ((finEquivZpowers x hx).apply_symm_apply a)
+-- TODO move
+lemma pow_finEquivZPowers_symm_apply {M} [Group M] (x : M) (hx) (a) :
+    x ^ ((finEquivZPowers x hx).symm a : ℕ) = a :=
+  congr_arg Subtype.val ((finEquivZPowers x hx).apply_symm_apply a)
 
 open Polynomial in
 lemma isTors' : Module.IsTorsionBySet ℤ[X]
@@ -336,8 +337,8 @@ lemma isTors' : Module.IsTorsionBySet ℤ[X]
     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]
-  simp only [pow_finEquivZpowers_symm_apply, coe_galRestrictHom_apply, AlgHom.coe_coe]
+    ← 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]
   rw [Finset.prod_set_coe (α := K ≃ₐ[k] K) (β := K) (f := fun i ↦ i ↑x) (Subgroup.zpowers σ)]
   congr
   ext x
@@ -751,8 +752,8 @@ lemma norm_eq_prod_pow_gen
     (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (η : K) :
     algebraMap k K (Algebra.norm k η) = (∏ i in Finset.range (orderOf σ), (σ ^ i) η)   := by
   rw [Algebra.norm_eq_prod_automorphisms, ← Fin.prod_univ_eq_prod_range,
-    ← (finEquivZpowers σ <| isOfFinOrder_of_finite _).symm.prod_comp]
-  simp only [pow_finEquivZpowers_symm_apply]
+    ← (finEquivZPowers σ <| isOfFinOrder_of_finite _).symm.prod_comp]
+  simp only [pow_finEquivZPowers_symm_apply]
   rw [Finset.prod_set_coe (α := K ≃ₐ[k] K) (β := K) (f := fun i ↦ i η) (Subgroup.zpowers σ)]
   congr; ext; simp [hσ]
 

FltRegular/NumberTheory/KummerExtension.lean

@@ -388,7 +388,7 @@ def autEquivZmod {ζ : K} (hζ : IsPrimitiveRoot ζ n) :
   (autEquivRootsOfUnity ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ H L hn).trans
     ((MulEquiv.subgroupCongr (IsPrimitiveRoot.zpowers_eq (k := ⟨n, hn⟩)
       (hζ.isUnit_unit' hn)).symm).trans (AddEquiv.toMultiplicative'
-        (hζ.isUnit_unit' hn).zmodEquivZpowers.symm))
+        (hζ.isUnit_unit' hn).zmodEquivZPowers.symm))
 
 lemma MulEquiv.subgroupCongr_apply {G} [Group G] {H₁ H₂ : Subgroup G} (e : H₁ = H₂) (x) :
   (MulEquiv.subgroupCongr e x : G) = x := rfl