α : Type ?u.2754
M₀ : Type ?u.2757
G₀ : Type u_1
M₀' : Type ?u.2763
G₀' : Type ?u.2766
F : Type ?u.2769
F' : Type ?u.2772
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b⁻¹) c
α : Type ?u.2754
M₀ : Type ?u.2757
G₀ : Type u_1
M₀' : Type ?u.2763
G₀' : Type ?u.2766
F : Type ?u.2769
F' : Type ?u.2772
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a / b) c
rw [div_eq_mul_inv]
no goals
α : Type ?u.2754
M₀ : Type ?u.2757
G₀ : Type u_1
M₀' : Type ?u.2763
G₀' : Type ?u.2766
F : Type ?u.2769
F' : Type ?u.2772
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b⁻¹) c
exact hac.mul_left hbc.inv_left₀