NoZeroSMulDivisors #
This file proves more lemmas about the NoZeroSMulDivisors class, which is deprecated in favor of
Module.IsTorsionFree.
@[instance 100]
instance GroupWithZero.toNoZeroSMulDivisors {R : Type u_1} {M : Type u_2} [GroupWithZero R] [AddMonoid M] [DistribMulAction R M] :
This instance applies to DivisionSemirings, in particular NNReal and NNRat.