feat(group_action/defs): generalize faithful actions (#8555)
This generalizes the `faithful_mul_semiring_action` typeclass to a mixin typeclass `has_faithful_scalar`, and provides instances for some simple actions:
* `has_faithful_scalar α α` (on cancellative monoids and monoids with zero)
* `has_faithful_scalar (opposite α) α`
* `has_faithful_scalar α (Π i, f i)`
* `has_faithful_scalar (units A) B`
* `has_faithful_scalar (equiv.perm α) α`
* `has_faithful_scalar M (α × β)`
* `has_faithful_scalar R (α →₀ M)`
* `has_faithful_scalar S (polynomial R)` (generalized from an existing instance)
* `has_faithful_scalar R (mv_polynomial σ S₁)`
* `has_faithful_scalar R (monoid_algebra k G)`
* `has_faithful_scalar R (add_monoid_algebra k G)`
As well as retaining the one other existing instance
* `faithful_mul_semiring_action ↥H E` where `H : subgroup (E ≃ₐ[F] E)`
The lemmas taking `faithful_mul_semiring_action` as a typeclass argument have been converted to use the new typeclass, but no attempt has been made to weaken their other hypotheses.
