Merge branch 'nightly-testing' of github.com:leanprover-community/mat…

…hlib4 into nightly-testing

Mathlib.lean

@@ -544,6 +544,10 @@ import Mathlib.Algebra.MvPolynomial.Rename
 import Mathlib.Algebra.MvPolynomial.Supported
 import Mathlib.Algebra.MvPolynomial.Variables
 import Mathlib.Algebra.NeZero
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Pi
+import Mathlib.Algebra.NoZeroSMulDivisors.Prod
 import Mathlib.Algebra.Notation
 import Mathlib.Algebra.Opposites
 import Mathlib.Algebra.Order.AbsoluteValue
@@ -4443,7 +4447,6 @@ import Mathlib.Tactic.ReduceModChar
 import Mathlib.Tactic.ReduceModChar.Ext
 import Mathlib.Tactic.Relation.Rfl
 import Mathlib.Tactic.Relation.Symm
-import Mathlib.Tactic.Relation.Trans
 import Mathlib.Tactic.Rename
 import Mathlib.Tactic.RenameBVar
 import Mathlib.Tactic.Replace

Mathlib/Algebra/Algebra/Basic.lean

@@ -9,6 +9,7 @@ import Mathlib.Algebra.Module.Equiv.Basic
 import Mathlib.Algebra.Module.Submodule.Ker
 import Mathlib.Algebra.Module.Submodule.RestrictScalars
 import Mathlib.Algebra.Module.ULift
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Ring.Subring.Basic
 import Mathlib.Data.Nat.Cast.Order.Basic
 import Mathlib.Data.Int.CharZero

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -5,7 +5,7 @@ Authors: Kexing Ying, Kevin Buzzard, Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
 import Mathlib.Algebra.Group.FiniteSupport
-import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Set.Subsingleton
 

Mathlib/Algebra/Group/EvenFunction.lean

@@ -3,9 +3,9 @@ Copyright (c) 2024 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
-import Mathlib.Algebra.Group.Action.Pi
-import Mathlib.Algebra.Module.Defs
 import Mathlib.Algebra.BigOperators.Group.Finset
+import Mathlib.Algebra.Group.Action.Pi
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 
 /-!
 # Even and odd functions

Mathlib/Algebra/ModEq.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Data.Int.ModEq
 import Mathlib.Algebra.Field.Basic
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.GroupTheory.QuotientGroup.Basic
 

Mathlib/Algebra/Module/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Field.Basic
 import Mathlib.Algebra.Group.Action.Pi
 import Mathlib.Algebra.Group.Indicator
 import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 
 /-!
 # Further basic results about modules.
@@ -95,30 +96,6 @@ theorem inv_intCast_smul_comm {α E : Type*} (R : Type*) [AddCommGroup E] [Divis
 @[deprecated (since := "2024-04-17")]
 alias inv_int_cast_smul_comm := inv_intCast_smul_comm
 
-
-
-section NoZeroSMulDivisors
-
-section Module
-
-instance [AddCommGroup M] [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M :=
-  ⟨fun {c x} hcx ↦ by rwa [← Nat.cast_smul_eq_nsmul ℤ c x, smul_eq_zero, Nat.cast_eq_zero] at hcx⟩
-
-end Module
-
-section GroupWithZero
-
-variable [GroupWithZero R] [AddMonoid M] [DistribMulAction R M]
-
--- see note [lower instance priority]
-/-- This instance applies to `DivisionSemiring`s, in particular `NNReal` and `NNRat`. -/
-instance (priority := 100) GroupWithZero.toNoZeroSMulDivisors : NoZeroSMulDivisors R M :=
-  ⟨fun {a _} h ↦ or_iff_not_imp_left.2 fun ha ↦ (smul_eq_zero_iff_eq <| Units.mk0 a ha).1 h⟩
-
-end GroupWithZero
-
-end NoZeroSMulDivisors
-
 namespace Function
 
 lemma support_smul_subset_left [Zero R] [Zero M] [SMulWithZero R M] (f : α → R) (g : α → M) :

Mathlib/Algebra/Module/Card.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.SetTheory.Cardinal.Basic
 
 /-!

Mathlib/Algebra/Module/Defs.lean

@@ -408,182 +408,6 @@ instance AddCommGroup.intIsScalarTower {R : Type u} {M : Type v} [Ring R] [AddCo
     [Module R M] : IsScalarTower ℤ R M where
   smul_assoc n x y := ((smulAddHom R M).flip y).map_zsmul x n
 
-section NoZeroSMulDivisors
-
-/-! ### `NoZeroSMulDivisors`
-
-This section defines the `NoZeroSMulDivisors` class, and includes some tests
-for the vanishing of elements (especially in modules over division rings).
--/
-
-
-/-- `NoZeroSMulDivisors R M` states that a scalar multiple is `0` only if either argument is `0`.
-This is a version of saying that `M` is torsion free, without assuming `R` is zero-divisor free.
-
-The main application of `NoZeroSMulDivisors R M`, when `M` is a module,
-is the result `smul_eq_zero`: a scalar multiple is `0` iff either argument is `0`.
-
-It is a generalization of the `NoZeroDivisors` class to heterogeneous multiplication.
--/
-@[mk_iff]
-class NoZeroSMulDivisors (R M : Type*) [Zero R] [Zero M] [SMul R M] : Prop where
-  /-- If scalar multiplication yields zero, either the scalar or the vector was zero. -/
-  eq_zero_or_eq_zero_of_smul_eq_zero : ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0
-
-export NoZeroSMulDivisors (eq_zero_or_eq_zero_of_smul_eq_zero)
-
-/-- Pullback a `NoZeroSMulDivisors` instance along an injective function. -/
-theorem Function.Injective.noZeroSMulDivisors {R M N : Type*} [Zero R] [Zero M] [Zero N]
-    [SMul R M] [SMul R N] [NoZeroSMulDivisors R N] (f : M → N) (hf : Function.Injective f)
-    (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c • x) = c • f x) : NoZeroSMulDivisors R M :=
-  ⟨fun {_ _} h =>
-    Or.imp_right (@hf _ _) <| h0.symm ▸ eq_zero_or_eq_zero_of_smul_eq_zero (by rw [← hs, h, h0])⟩
-
--- See note [lower instance priority]
-instance (priority := 100) NoZeroDivisors.toNoZeroSMulDivisors [Zero R] [Mul R]
-    [NoZeroDivisors R] : NoZeroSMulDivisors R R :=
-  ⟨fun {_ _} => eq_zero_or_eq_zero_of_mul_eq_zero⟩
-
-theorem smul_ne_zero [Zero R] [Zero M] [SMul R M] [NoZeroSMulDivisors R M] {c : R} {x : M}
-    (hc : c ≠ 0) (hx : x ≠ 0) : c • x ≠ 0 := fun h =>
-  (eq_zero_or_eq_zero_of_smul_eq_zero h).elim hc hx
-
-section SMulWithZero
-
-variable [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M}
-
-@[simp]
-theorem smul_eq_zero : c • x = 0 ↔ c = 0 ∨ x = 0 :=
-  ⟨eq_zero_or_eq_zero_of_smul_eq_zero, fun h =>
-    h.elim (fun h => h.symm ▸ zero_smul R x) fun h => h.symm ▸ smul_zero c⟩
-
-theorem smul_ne_zero_iff : c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0 := by rw [Ne, smul_eq_zero, not_or]
-
-lemma smul_eq_zero_iff_left (hx : x ≠ 0) : c • x = 0 ↔ c = 0 := by simp [hx]
-lemma smul_eq_zero_iff_right (hc : c ≠ 0) : c • x = 0 ↔ x = 0 := by simp [hc]
-lemma smul_ne_zero_iff_left (hx : x ≠ 0) : c • x ≠ 0 ↔ c ≠ 0 := by simp [hx]
-lemma smul_ne_zero_iff_right (hc : c ≠ 0) : c • x ≠ 0 ↔ x ≠ 0 := by simp [hc]
-
-end SMulWithZero
-
-section Module
-
-section Nat
-
-theorem Nat.noZeroSMulDivisors
-    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] :
-    NoZeroSMulDivisors ℕ M where
-  eq_zero_or_eq_zero_of_smul_eq_zero {c x} := by rw [← Nat.cast_smul_eq_nsmul R, smul_eq_zero]; simp
-
-theorem two_nsmul_eq_zero
-    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M]
-    {v : M} : 2 • v = 0 ↔ v = 0 := by
-  haveI := Nat.noZeroSMulDivisors R M
-  simp [smul_eq_zero]
-
-end Nat
-
-variable [Semiring R]
-variable (R M)
-
-/-- If `M` is an `R`-module with one and `M` has characteristic zero, then `R` has characteristic
-zero as well. Usually `M` is an `R`-algebra. -/
-theorem CharZero.of_module (M) [AddCommMonoidWithOne M] [CharZero M] [Module R M] : CharZero R := by
-  refine ⟨fun m n h => @Nat.cast_injective M _ _ _ _ ?_⟩
-  rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]
-
-end Module
-
-section AddCommGroup
-
--- `R` can still be a semiring here
-variable [Semiring R] [AddCommGroup M] [Module R M]
-
-section SMulInjective
-
-variable (M)
-
-theorem smul_right_injective [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) :
-    Function.Injective (c • · : M → M) :=
-  (injective_iff_map_eq_zero (smulAddHom R M c)).2 fun _ ha => (smul_eq_zero.mp ha).resolve_left hc
-
-variable {M}
-
-theorem smul_right_inj [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) {x y : M} :
-    c • x = c • y ↔ x = y :=
-  (smul_right_injective M hc).eq_iff
-
-end SMulInjective
-
-section Nat
-
-theorem self_eq_neg
-    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
-    {v : M} : v = -v ↔ v = 0 := by
-  rw [← two_nsmul_eq_zero R M, two_smul, add_eq_zero_iff_eq_neg]
-
-theorem neg_eq_self
-    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
-    {v : M} : -v = v ↔ v = 0 := by
-  rw [eq_comm, self_eq_neg R M]
-
-theorem self_ne_neg
-    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
-    {v : M} : v ≠ -v ↔ v ≠ 0 :=
-  (self_eq_neg R M).not
-
-theorem neg_ne_self
-    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
-    {v : M} : -v ≠ v ↔ v ≠ 0 :=
-  (neg_eq_self R M).not
-
-end Nat
-
-end AddCommGroup
-
-section Module
-
-variable [Ring R] [AddCommGroup M] [Module R M]
-
-section SMulInjective
-
-variable (R)
-variable [NoZeroSMulDivisors R M]
-
-theorem smul_left_injective {x : M} (hx : x ≠ 0) : Function.Injective fun c : R => c • x :=
-  fun c d h =>
-  sub_eq_zero.mp
-    ((smul_eq_zero.mp
-          (calc
-            (c - d) • x = c • x - d • x := sub_smul c d x
-            _ = 0 := sub_eq_zero.mpr h
-            )).resolve_right
-      hx)
-
-end SMulInjective
-
-instance [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M :=
-  ⟨fun {c x} hcx ↦ by rwa [← Nat.cast_smul_eq_nsmul ℤ, smul_eq_zero, Nat.cast_eq_zero] at hcx⟩
-
-variable (R M)
-
-theorem NoZeroSMulDivisors.int_of_charZero
-    (R) (M) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] :
-    NoZeroSMulDivisors ℤ M :=
-  ⟨fun {z x} h ↦ by simpa [← smul_one_smul R z x] using h⟩
-
-/-- Only a ring of characteristic zero can have a non-trivial module without additive or
-scalar torsion. -/
-theorem CharZero.of_noZeroSMulDivisors [Nontrivial M] [NoZeroSMulDivisors ℤ M] : CharZero R := by
-  refine ⟨fun {n m h} ↦ ?_⟩
-  obtain ⟨x, hx⟩ := exists_ne (0 : M)
-  replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h]
-  simpa using smul_left_injective ℤ hx h
-
-end Module
-
-end NoZeroSMulDivisors
-
 -- Porting note (#10618): simp can prove this
 --@[simp]
 theorem Nat.smul_one_eq_cast {R : Type*} [NonAssocSemiring R] (m : ℕ) : m • (1 : R) = ↑m := by

Mathlib/Algebra/Module/LinearMap/Basic.lean

@@ -5,7 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne
   Frédéric Dupuis, Heather Macbeth
 -/
 import Mathlib.Algebra.Module.LinearMap.Defs
-import Mathlib.Algebra.Module.Pi
+import Mathlib.Algebra.NoZeroSMulDivisors.Pi
 import Mathlib.GroupTheory.GroupAction.DomAct.Basic
 
 /-!

Mathlib/Algebra/Module/LinearMap/End.lean

@@ -6,6 +6,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne
 -/
 import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Algebra.Module.LinearMap.Defs
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 
 /-!
 # Endomorphisms of a module

Mathlib/Algebra/Module/Pi.lean

@@ -83,17 +83,4 @@ instance module' {g : I → Type*} {r : ∀ i, Semiring (f i)} {m : ∀ i, AddCo
     -- Porting note: not sure why `apply zero_smul` fails here.
     rw [zero_smul]
 
-instance noZeroSMulDivisors (α) [Semiring α] [∀ i, AddCommMonoid <| f i]
-    [∀ i, Module α <| f i] [∀ i, NoZeroSMulDivisors α <| f i] :
-    NoZeroSMulDivisors α (∀ i : I, f i) :=
-  ⟨fun {_ _} h =>
-    or_iff_not_imp_left.mpr fun hc =>
-      funext fun i => (smul_eq_zero.mp (congr_fun h i)).resolve_left hc⟩
-
-/-- A special case of `Pi.noZeroSMulDivisors` for non-dependent types. Lean struggles to
-synthesize this instance by itself elsewhere in the library. -/
-instance _root_.Function.noZeroSMulDivisors {ι α β : Type*} [Semiring α] [AddCommMonoid β]
-    [Module α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (ι → β) :=
-  Pi.noZeroSMulDivisors _
-
 end Pi

Mathlib/Algebra/Module/Prod.lean

@@ -35,17 +35,4 @@ instance instModule [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M
     add_smul := fun _ _ _ => mk.inj_iff.mpr ⟨add_smul _ _ _, add_smul _ _ _⟩
     zero_smul := fun _ => mk.inj_iff.mpr ⟨zero_smul _ _, zero_smul _ _⟩ }
 
-instance noZeroSMulDivisors {r : Semiring R} [AddCommMonoid M] [AddCommMonoid N]
-    [Module R M] [Module R N] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] :
-    NoZeroSMulDivisors R (M × N) :=
-  { eq_zero_or_eq_zero_of_smul_eq_zero := by -- Porting note: in mathlib3 there is no need for `by`/
-      -- `intro`/`exact`, i.e. the following works:
-      -- ⟨fun c ⟨x, y⟩ h =>
-      --   or_iff_not_imp_left.mpr fun hc =>
-      intro c ⟨x, y⟩ h
-      exact or_iff_not_imp_left.mpr fun hc =>
-        mk.inj_iff.mpr
-          ⟨(smul_eq_zero.mp (congr_arg fst h)).resolve_left hc,
-            (smul_eq_zero.mp (congr_arg snd h)).resolve_left hc⟩ }
-
 end Prod

Mathlib/Algebra/Module/Rat.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Module.Basic
+import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Field.Rat
 import Mathlib.Algebra.Order.Field.Rat