instNoZeroSMulDivisorsNatOfInt — Mathlib

English

If M is an additive group and NoZeroSMulDivisors ℤ M holds, then NoZeroSMulDivisors ℕ M holds as well.

Русский

Если M — аддитивная группа и выполняется NoZeroSMulDivisors ℤ M, то также выполняется NoZeroSMulDivisors ℕ M.

LaTeX

$$NoZeroSMulDivisors ℕ M$$

Lean4

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⟩

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