Commit 2021-08-06 21:15 2f29e090

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.