Faithful actions involving groups with zero #
@[deprecated "subsumed by `instFaithfulSMul`" (since := "2026-02-03")]
theorem
IsRightCancelMulZero.faithfulSMul
{α : Type u_1}
[MonoidWithZero α]
[IsRightCancelMulZero α]
:
FaithfulSMul α α
Monoid.toMulAction is faithful on nontrivial cancellative monoids with zero.