Merge branch 'master' into aliu/irreducible-comp

Author: plp127

Mathlib.lean

@@ -526,6 +526,7 @@ public import Mathlib.Algebra.GroupWithZero.Action.Pi
 public import Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
 public import Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
 public import Mathlib.Algebra.GroupWithZero.Action.Prod
+public import Mathlib.Algebra.GroupWithZero.Action.Regular
 public import Mathlib.Algebra.GroupWithZero.Action.TransferInstance
 public import Mathlib.Algebra.GroupWithZero.Action.Units
 public import Mathlib.Algebra.GroupWithZero.Associated
@@ -3980,6 +3981,7 @@ public import Mathlib.Data.Erased
 public import Mathlib.Data.FP.Basic
 public import Mathlib.Data.Fin.Basic
 public import Mathlib.Data.Fin.Embedding
+public import Mathlib.Data.Fin.EquivOfInjective
 public import Mathlib.Data.Fin.Fin2
 public import Mathlib.Data.Fin.FlagRange
 public import Mathlib.Data.Fin.Init
@@ -4357,6 +4359,7 @@ public import Mathlib.Data.Nat.Nth
 public import Mathlib.Data.Nat.NthRoot.Defs
 public import Mathlib.Data.Nat.Order.Lemmas
 public import Mathlib.Data.Nat.PSub
+public import Mathlib.Data.Nat.PadicValNat
 public import Mathlib.Data.Nat.Pairing
 public import Mathlib.Data.Nat.Periodic
 public import Mathlib.Data.Nat.Prime.Basic
@@ -4700,6 +4703,8 @@ public import Mathlib.FieldTheory.SplittingField.Construction
 public import Mathlib.FieldTheory.SplittingField.IsSplittingField
 public import Mathlib.FieldTheory.Tower
 public import Mathlib.FieldTheory.TranscendentalSeparable
+public import Mathlib.Geometry.Convex.AffineMap.Defs
+public import Mathlib.Geometry.Convex.AffineMap.Module
 public import Mathlib.Geometry.Convex.Cone.Basic
 public import Mathlib.Geometry.Convex.Cone.Dual
 public import Mathlib.Geometry.Convex.Cone.DualFinite
@@ -5011,6 +5016,7 @@ public import Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
 public import Mathlib.GroupTheory.SpecificGroups.Dihedral
 public import Mathlib.GroupTheory.SpecificGroups.KleinFour
 public import Mathlib.GroupTheory.SpecificGroups.Quaternion
+public import Mathlib.GroupTheory.SpecificGroups.VirtuallyCyclic
 public import Mathlib.GroupTheory.SpecificGroups.ZGroup
 public import Mathlib.GroupTheory.Subgroup.Center
 public import Mathlib.GroupTheory.Subgroup.Centralizer
@@ -5242,6 +5248,7 @@ public import Mathlib.LinearAlgebra.Matrix.BilinearForm
 public import Mathlib.LinearAlgebra.Matrix.Block
 public import Mathlib.LinearAlgebra.Matrix.Cartan
 public import Mathlib.LinearAlgebra.Matrix.Cartan.Basic
+public import Mathlib.LinearAlgebra.Matrix.Cartan.Realisation
 public import Mathlib.LinearAlgebra.Matrix.CharP
 public import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
 public import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
@@ -5446,6 +5453,7 @@ public import Mathlib.LinearAlgebra.Trace
 public import Mathlib.LinearAlgebra.Transvection
 public import Mathlib.LinearAlgebra.Transvection.Basic
 public import Mathlib.LinearAlgebra.Transvection.Generation
+public import Mathlib.LinearAlgebra.Unimodular
 public import Mathlib.LinearAlgebra.UnitaryGroup
 public import Mathlib.LinearAlgebra.Vandermonde
 public import Mathlib.Logic.Embedding.Basic

Mathlib/Algebra/EuclideanDomain/Defs.lean

@@ -88,7 +88,7 @@ class EuclideanDomain (R : Type u) extends CommRing R, Nontrivial R where
   protected r : R → R → Prop
   /-- The relation `r` must be well-founded.
     This ensures that the GCD algorithm always terminates. -/
-  r_wellFounded : WellFounded r
+  [r_wellFounded : WellFounded r]
   /-- The relation `r` satisfies `r (a % b) b`. -/
   protected remainder_lt : ∀ (a) {b}, b ≠ 0 → r (remainder a b) b
   /-- An additional constraint on `r`. -/
@@ -116,9 +116,6 @@ local instance wellFoundedRelation : WellFoundedRelation R where
   rel := EuclideanDomain.r
   wf := r_wellFounded
 
-instance isWellFounded : IsWellFounded R (· ≺ ·) where
-  wf := r_wellFounded
-
 -- see Note [lower instance priority]
 instance (priority := 70) : Div R :=
   ⟨EuclideanDomain.quotient⟩

Mathlib/Algebra/Group/Basic.lean

@@ -197,6 +197,14 @@ lemma mul_left_iterate_apply (a b : M) : (a * ·)^[n] b = a ^ n * b := by simp
 @[to_additive /-- Version of `add_right_iterate` that is fully applied, for `rw`. -/ ]
 lemma mul_right_iterate_apply (a b : M) : (· * a)^[n] b = b * a ^ n := by simp
 
+@[to_additive]
+lemma mul_left_iterate_apply_self (a : M) (n : ℕ) : (a * ·)^[n] a = a ^ (n + 1) := by
+  rw [pow_succ, mul_left_iterate_apply]
+
+@[to_additive]
+lemma mul_right_iterate_apply_self (a : M) (n : ℕ) : (· * a)^[n] a = a ^ (n + 1) := by
+  rw [pow_succ', mul_right_iterate_apply]
+
 @[to_additive]
 lemma mul_left_iterate_apply_one (a : M) : (a * ·)^[n] 1 = a ^ n := by simp
 

Mathlib/Algebra/Group/Fin/Basic.lean

@@ -70,7 +70,7 @@ instance addCommGroup (n : ℕ) [NeZero n] : AddCommGroup (Fin n) where
   neg_add_cancel := fun ⟨a, ha⟩ ↦
     Fin.ext <| (Nat.mod_add_mod _ _ _).trans <| by
       rw [Fin.val_zero, Nat.sub_add_cancel, Nat.mod_self]
-      exact le_of_lt ha
+      exact Nat.le_of_lt ha
   sub := Fin.sub
   sub_eq_add_neg := fun ⟨a, ha⟩ ⟨b, hb⟩ ↦
     Fin.ext <| by simp [Fin.sub_def, Fin.neg_def, Fin.add_def, Nat.add_comm]
@@ -126,13 +126,11 @@ lemma lt_sub_one_iff {k : Fin (n + 2)} : k < k - 1 ↔ k = 0 := by
 @[simp] lemma le_sub_one_iff {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 := by
   cases n
   · simp [fin_one_eq_zero k]
-  simp only [le_def]
-  rw [← lt_sub_one_iff, le_iff_lt_or_eq, val_fin_lt, val_inj, lt_sub_one_iff, or_iff_left_iff_imp,
-    eq_comm, sub_eq_iff_eq_add]
+  rw [le_def, Nat.le_iff_lt_or_eq, val_fin_lt, lt_sub_iff, val_inj, eq_comm, sub_eq_self]
   simp
 
 lemma sub_one_lt_iff {k : Fin (n + 1)} : k - 1 < k ↔ 0 < k :=
-  not_iff_not.1 <| by simp only [lt_def, not_lt, val_fin_le, le_sub_one_iff, le_zero_iff]
+  not_iff_not.1 <| by simp only [lt_def, Nat.not_lt, val_fin_le, le_sub_one_iff, le_zero_iff]
 
 @[simp] lemma neg_last (n : ℕ) : -Fin.last n = 1 := by simp [neg_eq_iff_add_eq_zero]
 

Mathlib/Algebra/Group/Subgroup/Map.lean

@@ -497,9 +497,17 @@ def subgroupComap (f : G →* G') (H' : Subgroup G') : H'.comap f →* H' :=
   f.submonoidComap H'.toSubmonoid
 
 @[to_additive]
-lemma subgroupComap_surjective_of_surjective (f : G →* G') (H' : Subgroup G') (hf : Surjective f) :
+lemma subgroupComap_surjective (f : G →* G') (H' : Subgroup G') (hf : Surjective f) :
     Surjective (f.subgroupComap H') :=
-  f.submonoidComap_surjective_of_surjective H'.toSubmonoid hf
+  f.submonoidComap_surjective H'.toSubmonoid hf
+
+@[to_additive (attr := deprecated (since := "2026-09-09"))]
+alias subgroupComap_surjective_of_surjective := subgroupComap_surjective
+
+@[to_additive]
+lemma subgroupComap_injective (f : G →* G') (H' : Subgroup G') (hf : Injective f) :
+    Injective (f.subgroupComap H') :=
+  f.submonoidComap_injective H'.toSubmonoid hf
 
 /-- The `MonoidHom` from a subgroup to its image. -/
 @[to_additive (attr := simps!) /-- the `AddMonoidHom` from an additive subgroup to its image -/]
@@ -511,6 +519,11 @@ theorem subgroupMap_surjective (f : G →* G') (H : Subgroup G) :
     Function.Surjective (f.subgroupMap H) :=
   f.submonoidMap_surjective H.toSubmonoid
 
+@[to_additive]
+theorem subgroupMap_injective (f : G →* G') (H : Subgroup G) (hf : Function.Injective f) :
+    Function.Injective (f.subgroupMap H) :=
+  f.submonoidMap_injective hf H.toSubmonoid
+
 end MonoidHom
 
 namespace MulEquiv

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -871,13 +871,21 @@ def submonoidComap (f : M →* N) (N' : Submonoid N) :
   map_mul' x y := Subtype.ext (f.map_mul x y)
 
 @[to_additive]
-lemma submonoidComap_surjective_of_surjective (f : M →* N) (N' : Submonoid N) (hf : Surjective f) :
+lemma submonoidComap_surjective (f : M →* N) (N' : Submonoid N) (hf : Surjective f) :
     Surjective (f.submonoidComap N') := fun y ↦ by
   obtain ⟨x, hx⟩ := hf y
   use ⟨x, mem_comap.mpr (hx ▸ y.2)⟩
   apply Subtype.val_injective
   simp [hx]
 
+@[to_additive (attr := deprecated (since := "2026-09-09"))]
+alias submonoidComap_surjective_of_surjective := submonoidComap_surjective
+
+@[to_additive]
+lemma submonoidComap_injective (f : M →* N) (N' : Submonoid N) (hf : Injective f) :
+    Injective (f.submonoidComap N') :=
+  fun _ _ h ↦ Subtype.ext (hf (congrArg Subtype.val h))
+
 /-- The `MonoidHom` from a `Submonoid` to its image.
 See `MulEquiv.SubmonoidMap` for a variant for `MulEquiv`s. -/
 @[to_additive (attr := simps)

Mathlib/Algebra/Group/UniqueProds/Basic.lean

@@ -433,8 +433,8 @@ open UniqueMul in
   uniqueMul_of_nonempty {A} := by
     classical
     let _ := isWellFounded_ssubset (α := ∀ i, G i) -- why need this?
-    apply IsWellFounded.induction (· ⊂ ·) A; intro A ihA B hA
-    apply IsWellFounded.induction (· ⊂ ·) B; intro B ihB hB
+    apply WellFounded.induction' (· ⊂ ·) A; intro A ihA B hA
+    apply WellFounded.induction' (· ⊂ ·) B; intro B ihB hB
     by_cases! +distrib hc : #A ≤ 1 ∧ #B ≤ 1
     · exact of_card_le_one hA hB hc.1 hc.2
     obtain ⟨i, hc⟩ := exists_or.mpr (hc.imp exists_of_one_lt_card_pi exists_of_one_lt_card_pi)
@@ -511,8 +511,8 @@ instance instForall {ι} (G : ι → Type*) [∀ i, Mul (G i)] [∀ i, TwoUnique
   uniqueMul_of_one_lt_card {A} := by
     classical
     let _ := isWellFounded_ssubset (α := ∀ i, G i) -- why need this?
-    apply IsWellFounded.induction (· ⊂ ·) A; intro A ihA B
-    apply IsWellFounded.induction (· ⊂ ·) B; intro B ihB hc
+    apply WellFounded.induction' (· ⊂ ·) A; intro A ihA B
+    apply WellFounded.induction' (· ⊂ ·) B; intro B ihB hc
     obtain ⟨hA, hB, hc⟩ := Nat.one_lt_mul_iff.mp hc
     rw [card_pos] at hA hB
     obtain ⟨i, hc⟩ := exists_or.mpr (hc.imp exists_of_one_lt_card_pi exists_of_one_lt_card_pi)

Mathlib/Algebra/GroupWithZero/Action/Regular.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2021 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+module
+
+public import Mathlib.Algebra.Regular.SMul
+public import Mathlib.Algebra.GroupWithZero.Action.Defs
+
+/-!
+# Results about `IsSMulRegular` for `MonoidWithZero`
+-/
+
+@[expose] public section
+
+variable {R S M : Type*} {a b : R} {s : S}
+
+namespace IsSMulRegular
+
+section MonoidWithZero
+variable [MonoidWithZero R] [Zero M] [MulActionWithZero R M]
+
+/-- The element `0` is `M`-regular if and only if `M` is trivial. -/
+protected theorem subsingleton (h : IsSMulRegular M (0 : R)) : Subsingleton M :=
+  ⟨fun a b => h (by dsimp only [Function.comp_def]; repeat' rw [MulActionWithZero.zero_smul])⟩
+
+/-- The element `0` is `M`-regular if and only if `M` is trivial. -/
+theorem zero_iff_subsingleton : IsSMulRegular M (0 : R) ↔ Subsingleton M :=
+  ⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩
+
+/-- The `0` element is not `M`-regular, on a non-trivial module. -/
+theorem not_zero_iff : ¬IsSMulRegular M (0 : R) ↔ Nontrivial M := by
+  rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff]
+  push Not
+  exact Iff.rfl
+
+/-- The element `0` is `M`-regular when `M` is trivial. -/
+theorem zero [sM : Subsingleton M] : IsSMulRegular M (0 : R) :=
+  zero_iff_subsingleton.mpr sM
+
+/-- The `0` element is not `M`-regular, on a non-trivial module. -/
+theorem not_zero [nM : Nontrivial M] : ¬IsSMulRegular M (0 : R) :=
+  not_zero_iff.mpr nM
+
+end MonoidWithZero
+
+end IsSMulRegular
+
+section SMulZeroClass
+
+protected lemma IsSMulRegular.right_eq_zero_of_smul [Zero M] [SMulZeroClass R M]
+    {r : R} {x : M} (h1 : IsSMulRegular M r) (h2 : r • x = 0) : x = 0 :=
+  h1 (h2.trans (smul_zero r).symm)
+
+end SMulZeroClass
+
+lemma isSMulRegular_iff_right_eq_zero_of_smul [AddGroup M] [DistribSMul R M] {r : R} :
+    IsSMulRegular M r ↔ ∀ m : M, r • m = 0 → m = 0 where
+  mp h _ := h.right_eq_zero_of_smul
+  mpr h m₁ m₂ eq := sub_eq_zero.mp <| h _ <| by simp_rw [smul_sub, eq, sub_self]
+
+alias ⟨_, IsSMulRegular.of_right_eq_zero_of_smul⟩ := isSMulRegular_iff_right_eq_zero_of_smul

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -6,10 +6,12 @@ Authors: Kenny Lau, Devon Tuma, Oliver Nash
 module
 
 public import Mathlib.Algebra.Group.Submonoid.Membership
+public import Mathlib.Algebra.GroupWithZero.Action.Defs
 public import Mathlib.Algebra.GroupWithZero.Associated
 public import Mathlib.Algebra.GroupWithZero.Regular
 public import Mathlib.Algebra.Regular.SMul
 public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
+import Mathlib.Algebra.GroupWithZero.Action.Regular
 
 /-!
 # Non-zero divisors and smul-divisors

Mathlib/Algebra/Lie/Engel.lean

@@ -254,7 +254,7 @@ theorem LieAlgebra.isEngelian_of_isNoetherian [IsNoetherian R L] : LieAlgebra.Is
     refine isNoetherian_of_surjective (LieHom.rangeRestrict (toEnd R L M)).toLinearMap ?_
     simp only [LinearMap.range_eq_top]
     exact LieHom.surjective_rangeRestrict (toEnd R L M)
-  obtain ⟨K, hK₁, hK₂⟩ := (LieSubalgebra.wellFoundedGT_of_noetherian R L').wf.has_min s hs
+  obtain ⟨K, hK₁, hK₂⟩ := (LieSubalgebra.wellFoundedGT_of_noetherian R L').has_min s hs
   obtain rfl : K = ⊤ := by grind
   exact hK₁