def AddMonoid.IsTorsionFree.noZeroNsmulDivisors {M : Type u_1} [AddMonoid M] (hM : AddMonoid.IsTorsionFree M) : NoZeroSMulDivisors ℕ M

See note [reducible non-instances].

Equations

• ⋯ = ⋯