instNoZeroSMulDivisorsNatOfInt_1 — Mathlib

English

If M is an additive group and NoZeroSMulDivisors Int M holds, then NoZeroSMulDivisors Nat M holds.

Русский

Если M — аддитивная группа и выполняется NoZeroSMulDivisors Int M, то NoZeroSMulDivisors Nat M.

LaTeX

$$NoZeroSMulDivisors Nat M$$

Lean4

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⟩

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