feat(group_theory/group_action/basic): Left multiplication satisfies …

…the `quotient_action` axiom (#13249) This PR adds an instance `quotient_action α H`, meaning that left multiplication satisfies the `quotient_action` axiom.
leanprover-community · Apr 9, 2022 · 1480161 · 1480161
1 parent 22b7d21
commit 1480161
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/group_theory/group_action/basic.lean b/src/group_theory/group_action/basic.lean
@@ -309,6 +309,9 @@ class _root_.add_action.quotient_action {α : Type*} (β : Type*) [add_group α]
 
 attribute [to_additive add_action.quotient_action] mul_action.quotient_action
 
+@[to_additive] instance left_quotient_action : quotient_action α H :=
+⟨λ _ _ _ _, by rwa [smul_eq_mul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]⟩
+
 end quotient_action
 
 open quotient_group