to_noZeroSMulDivisors_nat — Mathlib

English

If M is an AddMonoid with IsAddTorsionFree, then NoZeroSMulDivisors on the natural action holds: for all n in ℕ and x in M, n · x = 0 implies n = 0 or x = 0.

Русский

Если M — аддитивный моноид с условием IsAddTorsionFree, то для ℕ-модуля выполняется: для всех n ∈ ℕ и x ∈ M, n · x = 0 влечёт n = 0 или x = 0.

LaTeX

$$$$\forall n \in \mathbb{N}, \forall x \in M, n \cdot x = 0 \Rightarrow n = 0 \lor x = 0.$$$$

Lean4

instance to_noZeroSMulDivisors_nat [AddMonoid M] [IsAddTorsionFree M] : NoZeroSMulDivisors ℕ M where
  eq_zero_or_eq_zero_of_smul_eq_zero {n x} hx := by contrapose! hx; simpa using (nsmul_right_injective hx.1).ne hx.2

Похожие утверждения