mathlib

65b5dd8b - feat(group_theory/transversal): A `quotient_action` induces an action on left transversals (#13282)

feat(group_theory/transversal): A `quotient_action` induces an action on left transversals (#13282) A `quotient_action` induces an action on left transversals. Once #13283 is merged, I'll PR some more API generalizing the existing lemma `smul_symm_apply_eq_mul_symm_apply_inv_smul`.