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.