F : Type ?u.56322
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ ↑T (↑S (a * b)) = ↑S (↑T (a * b))
F : Type ?u.56322
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ (↑T ∘ ↑S) (a * b) = (↑S ∘ ↑T) (a * b)
simp
no goals
F : Type ?u.56322
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ ↑T (↑S (a * b)) = ↑S (↑T (a * b))
rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]