feat(group_theory/group_action/basic): Add typeclass for actions that descend to the quotient (#12999)
feat(group_theory/group_action/basic): Add typeclass for actions that descend to the quotient (#12999)

Part of #12848.





leanprover-community/mathlib,leanprover-community/mathlib