Trigger CI for leanprover-community/batteries#1028

Mathlib.lean

@@ -2981,6 +2981,7 @@ import Mathlib.GroupTheory.DoubleCoset
 import Mathlib.GroupTheory.EckmannHilton
 import Mathlib.GroupTheory.Exponent
 import Mathlib.GroupTheory.FiniteAbelian.Basic
+import Mathlib.GroupTheory.FiniteAbelian.Duality
 import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.FixedPointFree
 import Mathlib.GroupTheory.Frattini
@@ -4276,6 +4277,7 @@ import Mathlib.RingTheory.Presentation
 import Mathlib.RingTheory.Prime
 import Mathlib.RingTheory.PrimeSpectrum
 import Mathlib.RingTheory.PrincipalIdealDomain
+import Mathlib.RingTheory.PrincipalIdealDomainOfPrime
 import Mathlib.RingTheory.QuotSMulTop
 import Mathlib.RingTheory.Radical
 import Mathlib.RingTheory.ReesAlgebra

Mathlib/GroupTheory/FiniteAbelian/Basic.lean

@@ -14,7 +14,7 @@ import Mathlib.Data.ZMod.Quotient
   `p i ^ e i`.
 * `AddCommGroup.equiv_directSum_zmod_of_finite` : Any finite abelian group is a direct sum of
   some `ZMod (p i ^ e i)` for some prime powers `p i ^ e i`.
-
+* `CommGroup.equiv_prod_multiplicative_zmod_of_finite` is a version for multiplicative groups.
 -/
 
 open scoped DirectSum
@@ -139,7 +139,7 @@ theorem equiv_directSum_zmod_of_finite [Finite G] :
             ⟨Finsupp.single 0 a, Finsupp.single_eq_same⟩).false.elim
 
 /-- **Structure theorem of finite abelian groups** : Any finite abelian group is a direct sum of
-some `ZMod (q i)` for some prime powers `q i > 1`. -/
+some `ZMod (n i)` for some natural numbers `n i > 1`. -/
 lemma equiv_directSum_zmod_of_finite' (G : Type*) [AddCommGroup G] [Finite G] :
     ∃ (ι : Type) (_ : Fintype ι) (n : ι → ℕ),
       (∀ i, 1 < n i) ∧ Nonempty (G ≃+ ⨁ i, ZMod (n i)) := by
@@ -161,9 +161,9 @@ namespace CommGroup
 theorem finite_of_fg_torsion [CommGroup G] [Group.FG G] (hG : Monoid.IsTorsion G) : Finite G :=
   @Finite.of_equiv _ _ (AddCommGroup.finite_of_fg_torsion (Additive G) hG) Multiplicative.ofAdd
 
-/-- The **Classification Theorem For Finite Abelian Groups** in a multiplicative version:
+/-- The **Structure Theorem For Finite Abelian Groups** in a multiplicative version:
 A finite commutative group `G` is isomorphic to a finite product of finite cyclic groups. -/
-theorem equiv_prod_multiplicative_zmod (G : Type*) [CommGroup G] [Finite G] :
+theorem equiv_prod_multiplicative_zmod_of_finite (G : Type*) [CommGroup G] [Finite G] :
     ∃ (ι : Type) (_ : Fintype ι) (n : ι → ℕ),
        (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i)))) := by
   obtain ⟨ι, inst, n, h₁, h₂⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' (Additive G)

Mathlib/GroupTheory/FiniteAbelian/Duality.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2024 Michael Stoll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Stoll
+-/
+import Mathlib.GroupTheory.FiniteAbelian.Basic
+import Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
+
+/-!
+# Duality for finite abelian groups
+
+Let `G` be a finite abelian group and let `M` be a commutative monoid that has enough `n`th roots
+of unity, where `n` is the exponent of `G`. The main results in this file are
+* `CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity`: Homomorphisms `G →* Mˣ` separate
+  elements of `G`.
+* `CommGroup.monoidHom_mulEquiv_self_of_hasEnoughRootsOfUnity`: `G` is isomorphic to `G →* Mˣ`.
+-/
+
+namespace CommGroup
+
+open MonoidHom
+
+private
+lemma dvd_exponent {ι G : Type*} [Finite ι] [CommGroup G] {n : ι → ℕ}
+    (e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))) (i : ι) :
+  n i ∣ Monoid.exponent G := by
+  classical -- to get `DecidableEq ι`
+  have : n i = orderOf (e.symm <| Pi.mulSingle i <| .ofAdd 1) := by
+    simpa only [MulEquiv.orderOf_eq, orderOf_piMulSingle, orderOf_ofAdd_eq_addOrderOf]
+      using (ZMod.addOrderOf_one (n i)).symm
+  exact this ▸ Monoid.order_dvd_exponent _
+
+variable (G M : Type*) [CommGroup G] [Finite G] [CommMonoid M]
+
+private
+lemma exists_apply_ne_one_aux (H : ∀ n : ℕ, n ∣ Monoid.exponent G → ∀ a : ZMod n, a ≠ 0 →
+    ∃ φ : Multiplicative (ZMod n) →* M, φ (.ofAdd a) ≠ 1)
+    {a : G} (ha : a ≠ 1) :
+    ∃ φ : G →* M, φ a ≠ 1 := by
+  obtain ⟨ι, _, n, _, h⟩ := CommGroup.equiv_prod_multiplicative_zmod_of_finite G
+  let e := h.some
+  obtain ⟨i, hi⟩ : ∃ i : ι, e a i ≠ 1 := by
+    contrapose! ha
+    exact (MulEquiv.map_eq_one_iff e).mp <| funext ha
+  have hi : Multiplicative.toAdd (e a i) ≠ 0 := by
+    simp only [ne_eq, toAdd_eq_zero, hi, not_false_eq_true]
+  obtain ⟨φi, hφi⟩ := H (n i) (dvd_exponent e i) (Multiplicative.toAdd <| e a i) hi
+  use (φi.comp (Pi.evalMonoidHom (fun (i : ι) ↦ Multiplicative (ZMod (n i))) i)).comp e
+  simpa only [coe_comp, coe_coe, Function.comp_apply, Pi.evalMonoidHom_apply, ne_eq] using hφi
+
+variable [HasEnoughRootsOfUnity M (Monoid.exponent G)]
+
+/-- If `G` is a finite commutative group of exponent `n` and `M` is a commutative monoid
+with enough `n`th roots of unity, then for each `a ≠ 1` in `G`, there exists a
+group homomorphism `φ : G → Mˣ` such that `φ a ≠ 1`. -/
+theorem exists_apply_ne_one_of_hasEnoughRootsOfUnity {a : G} (ha : a ≠ 1) :
+    ∃ φ : G →* Mˣ, φ a ≠ 1 := by
+  refine exists_apply_ne_one_aux G Mˣ (fun n hn a ha₀ ↦ ?_) ha
+  have : NeZero n := ⟨fun H ↦ NeZero.ne _ <| Nat.eq_zero_of_zero_dvd (H ▸ hn)⟩
+  have := HasEnoughRootsOfUnity.of_dvd M hn
+  exact ZMod.exists_monoidHom_apply_ne_one (HasEnoughRootsOfUnity.exists_primitiveRoot M n) ha₀
+
+/-- A finite commutative group `G` is (noncanonically) isomorphic to the group `G →* Mˣ`
+when `M` is a commutative monoid with enough `n`th roots of unity, where `n` is the exponent
+of `G`. -/
+theorem mulEquiv_monoidHom_of_hasEnoughRootsOfUnity : Nonempty (G ≃* (G →* Mˣ)) := by
+  classical -- to get `DecidableEq ι`
+  obtain ⟨ι, _, n, ⟨h₁, h₂⟩⟩ := equiv_prod_multiplicative_zmod_of_finite G
+  let e := h₂.some
+  let e' := Pi.monoidHomMulEquiv (fun i ↦ Multiplicative (ZMod (n i))) Mˣ
+  let e'' := MulEquiv.monoidHomCongr e (.refl Mˣ)
+  have : ∀ i, NeZero (n i) := fun i ↦ NeZero.of_gt (h₁ i)
+  have inst i : HasEnoughRootsOfUnity M <| Nat.card <| Multiplicative <| ZMod (n i) := by
+    have hdvd : Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G := by
+      simpa only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card]
+        using dvd_exponent e i
+    exact HasEnoughRootsOfUnity.of_dvd M hdvd
+  let E i := (IsCyclic.monoidHom_equiv_self (Multiplicative (ZMod (n i))) M).some
+  exact ⟨e.trans (MulEquiv.piCongrRight E).symm|>.trans e'.symm|>.trans e''.symm⟩
+
+end CommGroup

Mathlib/GroupTheory/Sylow.lean

@@ -396,8 +396,9 @@ theorem card_sylow_dvd_index [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
   ((congr_arg _ (card_sylow_eq_index_normalizer P)).mp dvd_rfl).trans
     (index_dvd_of_le le_normalizer)
 
-theorem not_dvd_index_sylow' [hp : Fact p.Prime] (P : Sylow p G) [(P : Subgroup G).Normal]
-    [fP : FiniteIndex (P : Subgroup G)] : ¬p ∣ (P : Subgroup G).index := by
+/-- Auxilliary lemma for `Sylow.not_dvd_index` which is strictly stronger. -/
+private theorem Sylow.not_dvd_index_aux [hp : Fact p.Prime] (P : Sylow p G) [P.Normal]
+    [P.FiniteIndex] : ¬ p ∣ P.index := by
   intro h
   rw [index_eq_card (P : Subgroup G)] at h
   obtain ⟨x, hx⟩ := exists_prime_orderOf_dvd_card' (G := G ⧸ (P : Subgroup G)) p h
@@ -413,15 +414,27 @@ theorem not_dvd_index_sylow' [hp : Fact p.Prime] (P : Sylow p G) [(P : Subgroup
     QuotientGroup.ker_mk'] at hp
   exact hp.ne' (P.3 hQ hp.le)
 
-theorem not_dvd_index_sylow [hp : Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
-    (hP : relindex ↑P (P : Subgroup G).normalizer ≠ 0) : ¬p ∣ (P : Subgroup G).index := by
+/-- A Sylow p-subgroup has index indivisible by `p`, assuming [N(P) : P] < ∞. -/
+theorem Sylow.not_dvd_index' [hp : Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
+    (hP : P.relindex P.normalizer ≠ 0) : ¬ p ∣ P.index := by
   rw [← relindex_mul_index le_normalizer, ← card_sylow_eq_index_normalizer]
   haveI : (P.subtype le_normalizer : Subgroup (P : Subgroup G).normalizer).Normal :=
     Subgroup.normal_in_normalizer
   haveI : FiniteIndex ↑(P.subtype le_normalizer : Subgroup (P : Subgroup G).normalizer) := ⟨hP⟩
-  replace hP := not_dvd_index_sylow' (P.subtype le_normalizer)
+  replace hP := not_dvd_index_aux (P.subtype le_normalizer)
   exact hp.1.not_dvd_mul hP (not_dvd_card_sylow p G)
 
+@[deprecated (since := "2024-11-03")]
+alias not_dvd_index_sylow := Sylow.not_dvd_index'
+
+/-- A Sylow p-subgroup has index indivisible by `p`. -/
+theorem Sylow.not_dvd_index [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) [P.FiniteIndex] :
+    ¬ p ∣ P.index :=
+  P.not_dvd_index' Nat.card_pos.ne'
+
+@[deprecated (since := "2024-11-03")]
+alias not_dvd_index_sylow' := Sylow.not_dvd_index
+
 /-- **Frattini's Argument**: If `N` is a normal subgroup of `G`, and if `P` is a Sylow `p`-subgroup
   of `N`, then `N_G(P) ⊔ N = G`. -/
 theorem Sylow.normalizer_sup_eq_top {p : ℕ} [Fact p.Prime] {N : Subgroup G} [N.Normal]
@@ -636,8 +649,7 @@ lemma exists_subgroup_le_card_le {k p : ℕ} (hp : p.Prime) (h : IsPGroup p G) {
 theorem pow_dvd_card_of_pow_dvd_card [Finite G] {p n : ℕ} [hp : Fact p.Prime] (P : Sylow p G)
     (hdvd : p ^ n ∣ Nat.card G) : p ^ n ∣ Nat.card P := by
   rw [← index_mul_card P.1] at hdvd
-  exact (hp.1.coprime_pow_of_not_dvd
-    (not_dvd_index_sylow P index_ne_zero_of_finite)).symm.dvd_of_dvd_mul_left hdvd
+  exact (hp.1.coprime_pow_of_not_dvd P.not_dvd_index).symm.dvd_of_dvd_mul_left hdvd
 
 theorem dvd_card_of_dvd_card [Finite G] {p : ℕ} [Fact p.Prime] (P : Sylow p G)
     (hdvd : p ∣ Nat.card G) : p ∣ Nat.card P := by
@@ -649,7 +661,7 @@ theorem dvd_card_of_dvd_card [Finite G] {p : ℕ} [Fact p.Prime] (P : Sylow p G)
 theorem card_coprime_index [Finite G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G) :
     (Nat.card P).Coprime (index (P : Subgroup G)) :=
   let ⟨_n, hn⟩ := IsPGroup.iff_card.mp P.2
-  hn.symm ▸ (hp.1.coprime_pow_of_not_dvd (not_dvd_index_sylow P index_ne_zero_of_finite)).symm
+  hn.symm ▸ (hp.1.coprime_pow_of_not_dvd P.not_dvd_index).symm
 
 theorem ne_bot_of_dvd_card [Finite G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G)
     (hdvd : p ∣ Nat.card G) : (P : Subgroup G) ≠ ⊥ := by

Mathlib/GroupTheory/Transfer.lean

@@ -222,10 +222,7 @@ theorem transferSylow_restrict_eq_pow : ⇑((transferSylow P hP).restrict (P : S
 complement. -/
 theorem ker_transferSylow_isComplement' : IsComplement' (transferSylow P hP).ker P := by
   have hf : Function.Bijective ((transferSylow P hP).restrict (P : Subgroup G)) :=
-    (transferSylow_restrict_eq_pow P hP).symm ▸
-      (P.2.powEquiv'
-          (not_dvd_index_sylow P
-            (mt index_eq_zero_of_relindex_eq_zero index_ne_zero_of_finite))).bijective
+    (transferSylow_restrict_eq_pow P hP).symm ▸ (P.2.powEquiv' P.not_dvd_index).bijective
   rw [Function.Bijective, ← range_top_iff_surjective, restrict_range] at hf
   have := range_top_iff_surjective.mp (top_le_iff.mp (hf.2.ge.trans
     (map_le_range (transferSylow P hP) P)))
@@ -235,8 +232,7 @@ theorem ker_transferSylow_isComplement' : IsComplement' (transferSylow P hP).ker
   exact isComplement'_of_disjoint_and_mul_eq_univ (disjoint_iff.2 hf.1) hf.2
 
 theorem not_dvd_card_ker_transferSylow : ¬p ∣ Nat.card (transferSylow P hP).ker :=
-  (ker_transferSylow_isComplement' P hP).index_eq_card ▸ not_dvd_index_sylow P <|
-    mt index_eq_zero_of_relindex_eq_zero index_ne_zero_of_finite
+  (ker_transferSylow_isComplement' P hP).index_eq_card ▸ P.not_dvd_index
 
 theorem ker_transferSylow_disjoint (Q : Subgroup G) (hQ : IsPGroup p Q) :
     Disjoint (transferSylow P hP).ker Q :=

Mathlib/RingTheory/LocalProperties/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
+import Mathlib.RingTheory.Ideal.Colon
 import Mathlib.RingTheory.Localization.AtPrime
 import Mathlib.RingTheory.Localization.BaseChange
 import Mathlib.RingTheory.Localization.Submodule

Mathlib/RingTheory/LocalProperties/Submodule.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang, David Swinarski
 -/
 import Mathlib.Algebra.Module.LocalizedModule.Submodule
+import Mathlib.RingTheory.Ideal.Colon
 import Mathlib.RingTheory.Localization.AtPrime
 
 /-!

Mathlib/RingTheory/MaximalSpectrum.lean

@@ -3,8 +3,9 @@ Copyright (c) 2022 David Kurniadi Angdinata. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Kurniadi Angdinata
 -/
-import Mathlib.RingTheory.PrimeSpectrum
+import Mathlib.RingTheory.Ideal.Colon
 import Mathlib.RingTheory.Localization.AsSubring
+import Mathlib.RingTheory.PrimeSpectrum
 
 /-!
 # Maximal spectrum of a commutative ring

Mathlib/RingTheory/PrincipalIdealDomain.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Morenikeji Neri
 -/
 import Mathlib.Algebra.EuclideanDomain.Field
-import Mathlib.RingTheory.Ideal.Colon
 import Mathlib.RingTheory.UniqueFactorizationDomain
 
 /-!
@@ -504,52 +503,4 @@ theorem nonPrincipals_zorn (c : Set (Ideal R)) (hs : c ⊆ nonPrincipals R)
   rw [← hsSupJ, hx, nonPrincipals_def] at hs
   exact hs ⟨⟨x, rfl⟩⟩
 
-/-- If all prime ideals in a commutative ring are principal, so are all other ideals. -/
-theorem IsPrincipalIdealRing.of_prime (H : ∀ P : Ideal R, P.IsPrime → P.IsPrincipal) :
-    IsPrincipalIdealRing R := by
-  -- Suppose the set of `nonPrincipals` is not empty.
-  rw [← nonPrincipals_eq_empty_iff, Set.eq_empty_iff_forall_not_mem]
-  intro J hJ
-  -- We will show a maximal element `I ∈ nonPrincipals R` (which exists by Zorn) is prime.
-  obtain ⟨I, hJI, hI⟩ := zorn_le_nonempty₀ (nonPrincipals R) nonPrincipals_zorn _ hJ
-
-  have Imax' : ∀ {J}, I < J → J.IsPrincipal := by
-    intro K hK
-    simpa [nonPrincipals] using hI.not_prop_of_gt hK
-
-  by_cases hI1 : I = ⊤
-  · subst hI1
-    exact hI.prop top_isPrincipal
-  -- Let `x y : R` with `x * y ∈ I` and suppose WLOG `y ∉ I`.
-  refine hI.prop (H I ⟨hI1, fun {x y} hxy => or_iff_not_imp_right.mpr fun hy => ?_⟩)
-  obtain ⟨a, ha⟩ : (I ⊔ span {y}).IsPrincipal :=
-    Imax' (left_lt_sup.mpr (mt I.span_singleton_le_iff_mem.mp hy))
-  -- Then `x ∈ I.colon (span {y})`, which is equal to `I` if it's not principal.
-  suffices He : ¬(I.colon (span {y})).IsPrincipal by
-    rw [hI.eq_of_le ((nonPrincipals_def R).2 He) fun a ha ↦
-      Ideal.mem_colon_singleton.2 (mul_mem_right _ _ ha)]
-    exact Ideal.mem_colon_singleton.2 hxy
-  -- So suppose for the sake of contradiction that both `I ⊔ span {y}` and `I.colon (span {y})`
-  -- are principal.
-  rintro ⟨b, hb⟩
-  -- We will show `I` is generated by `a * b`.
-  refine (nonPrincipals_def _).1 hI.prop ⟨a * b, ?_⟩
-  refine
-    le_antisymm (α := Ideal R) (fun i hi => ?_) <|
-      (span_singleton_mul_span_singleton a b).ge.trans ?_
-  · have hisup : i ∈ I ⊔ span {y} := Ideal.mem_sup_left hi
-    have : y ∈ I ⊔ span {y} := Ideal.mem_sup_right (Ideal.mem_span_singleton_self y)
-    erw [ha, mem_span_singleton'] at hisup this
-    obtain ⟨v, rfl⟩ := this
-    obtain ⟨u, rfl⟩ := hisup
-    have hucolon : u ∈ I.colon (span {v * a}) := by
-      rw [Ideal.mem_colon_singleton, mul_comm v, ← mul_assoc]
-      exact mul_mem_right _ _ hi
-    erw [hb, mem_span_singleton'] at hucolon
-    obtain ⟨z, rfl⟩ := hucolon
-    exact mem_span_singleton'.2 ⟨z, by ring⟩
-  · rw [← Ideal.submodule_span_eq, ← ha, Ideal.sup_mul, sup_le_iff,
-      span_singleton_mul_span_singleton, mul_comm y, Ideal.span_singleton_le_iff_mem]
-    exact ⟨mul_le_right, Ideal.mem_colon_singleton.1 <| hb.symm ▸ Ideal.mem_span_singleton_self b⟩
-
 end PrincipalOfPrime

Mathlib/RingTheory/PrincipalIdealDomainOfPrime.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+import Mathlib.RingTheory.Ideal.Colon
+import Mathlib.RingTheory.PrincipalIdealDomain
+
+/-!
+# Principal ideal domains and prime ideals
+
+# Main results
+
+- `IsPrincipalIdeal.of_prime`: a ring where all prime ideals are principal is a principal ideal ring
+-/
+
+open Ideal
+
+variable {R : Type*} [CommRing R]
+
+/-- If all prime ideals in a commutative ring are principal, so are all other ideals. -/
+theorem IsPrincipalIdealRing.of_prime (H : ∀ P : Ideal R, P.IsPrime → P.IsPrincipal) :
+    IsPrincipalIdealRing R := by
+  -- Suppose the set of `nonPrincipals` is not empty.
+  rw [← nonPrincipals_eq_empty_iff, Set.eq_empty_iff_forall_not_mem]
+  intro J hJ
+  -- We will show a maximal element `I ∈ nonPrincipals R` (which exists by Zorn) is prime.
+  obtain ⟨I, hJI, hI⟩ := zorn_le_nonempty₀ (nonPrincipals R) nonPrincipals_zorn _ hJ
+
+  have Imax' : ∀ {J}, I < J → J.IsPrincipal := by
+    intro K hK
+    simpa [nonPrincipals] using hI.not_prop_of_gt hK
+
+  by_cases hI1 : I = ⊤
+  · subst hI1
+    exact hI.prop top_isPrincipal
+  -- Let `x y : R` with `x * y ∈ I` and suppose WLOG `y ∉ I`.
+  refine hI.prop (H I ⟨hI1, fun {x y} hxy => or_iff_not_imp_right.mpr fun hy => ?_⟩)
+  obtain ⟨a, ha⟩ : (I ⊔ span {y}).IsPrincipal :=
+    Imax' (left_lt_sup.mpr (mt I.span_singleton_le_iff_mem.mp hy))
+  -- Then `x ∈ I.colon (span {y})`, which is equal to `I` if it's not principal.
+  suffices He : ¬(I.colon (span {y})).IsPrincipal by
+    rw [hI.eq_of_le ((nonPrincipals_def R).2 He) fun a ha ↦
+      Ideal.mem_colon_singleton.2 (mul_mem_right _ _ ha)]
+    exact Ideal.mem_colon_singleton.2 hxy
+  -- So suppose for the sake of contradiction that both `I ⊔ span {y}` and `I.colon (span {y})`
+  -- are principal.
+  rintro ⟨b, hb⟩
+  -- We will show `I` is generated by `a * b`.
+  refine (nonPrincipals_def _).1 hI.prop ⟨a * b, ?_⟩
+  refine
+    le_antisymm (α := Ideal R) (fun i hi => ?_) <|
+      (span_singleton_mul_span_singleton a b).ge.trans ?_
+  · have hisup : i ∈ I ⊔ span {y} := Ideal.mem_sup_left hi
+    have : y ∈ I ⊔ span {y} := Ideal.mem_sup_right (Ideal.mem_span_singleton_self y)
+    erw [ha, mem_span_singleton'] at hisup this
+    obtain ⟨v, rfl⟩ := this
+    obtain ⟨u, rfl⟩ := hisup
+    have hucolon : u ∈ I.colon (span {v * a}) := by
+      rw [Ideal.mem_colon_singleton, mul_comm v, ← mul_assoc]
+      exact mul_mem_right _ _ hi
+    erw [hb, mem_span_singleton'] at hucolon
+    obtain ⟨z, rfl⟩ := hucolon
+    exact mem_span_singleton'.2 ⟨z, by ring⟩
+  · rw [← Ideal.submodule_span_eq, ← ha, Ideal.sup_mul, sup_le_iff,
+      span_singleton_mul_span_singleton, mul_comm y, Ideal.span_singleton_le_iff_mem]
+    exact ⟨mul_le_right, Ideal.mem_colon_singleton.1 <| hb.symm ▸ Ideal.mem_span_singleton_self b⟩

Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean

@@ -82,7 +82,7 @@ section cyclic
 
 /-- The group of group homomorphims from a finite cyclic group `G` of order `n` into the
 group of units of a ring `M` with all roots of unity is isomorphic to `G` -/
-lemma monoidHom_equiv_self (G M : Type*) [CommGroup G] [Finite G]
+lemma IsCyclic.monoidHom_equiv_self (G M : Type*) [CommGroup G] [Finite G]
     [IsCyclic G] [CommMonoid M] [HasEnoughRootsOfUnity M (Nat.card G)] :
     Nonempty ((G →* Mˣ) ≃* G) := by
   have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩

Mathlib/RingTheory/SimpleModule.lean

@@ -3,12 +3,13 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
+import Mathlib.LinearAlgebra.FiniteDimensional
 import Mathlib.LinearAlgebra.Isomorphisms
 import Mathlib.LinearAlgebra.Projection
 import Mathlib.Order.Atoms.Finite
-import Mathlib.Order.JordanHolder
 import Mathlib.Order.CompactlyGenerated.Intervals
-import Mathlib.LinearAlgebra.FiniteDimensional
+import Mathlib.Order.JordanHolder
+import Mathlib.RingTheory.Ideal.Colon
 
 /-!
 # Simple Modules