comp_mul_comm — Mathlib

English

Let T,S ∈ CentroidHom α. Then for all a,b ∈ α, (T ∘ S)(a b) = (S ∘ T)(a b).

Русский

Пусть T,S ∈ CentroidHom α. Тогда для всех a,b ∈ α выполняется (T ∘ S)(a b) = (S ∘ T)(a b).

LaTeX

$$$ (T \circ S)(a b) = (S \circ T)(a b) $$$

Lean4

theorem comp_mul_comm (T S : CentroidHom α) (a b : α) : (T ∘ S) (a * b) = (S ∘ T) (a * b) :=
  by
  simp only [Function.comp_apply]
  rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]

Похожие утверждения