Faithful actions involving groups with zero

instance IsRightCancelMulZero.faithfulSMul {α : Type u_1} [MonoidWithZero α] [IsRightCancelMulZero α] : FaithfulSMul α α

Monoid.toMulAction is faithful on nontrivial cancellative monoids with zero.