to_noZeroSMulDivisors_int — Mathlib

English

If G is an AddGroup with IsAddTorsionFree, then NoZeroSMulDivisors ℤ G holds: for all n ∈ ℤ and x ∈ G, n · x = 0 implies n = 0 or x = 0.

Русский

Если G — аддитивная группа с IsAddTorsionFree, то NoZeroSMulDivisors ℤ G выполняется: для всех n ∈ ℤ и x ∈ G, n · x = 0 влечёт n = 0 или x = 0.

LaTeX

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

Lean4

instance to_noZeroSMulDivisors_int [AddGroup G] [IsAddTorsionFree G] : NoZeroSMulDivisors ℤ G where
  eq_zero_or_eq_zero_of_smul_eq_zero {n x} hx := by contrapose! hx; simpa using (zsmul_right_injective hx.1).ne hx.2

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