Faithful actions involving groups with zero

instance CancelMonoidWithZero.faithfulSMul {α : Type u_1} [CancelMonoidWithZero α] [Nontrivial α] : FaithfulSMul α α

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