Faithful actions involving groups with zero #
instance
CancelMonoidWithZero.faithfulSMul
{α : Type u_5}
[CancelMonoidWithZero α]
[Nontrivial α]
:
FaithfulSMul α α
Monoid.toMulAction is faithful on nontrivial cancellative monoids with zero.
Equations
- ⋯ = ⋯