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.