mulRight_mul — Mathlib

English

Right multiplication by the product equals the composition of right multiplications: mulRight R (a b) = (mulRight R b) ∘ (mulRight R a).

Русский

Правое умножение на произведение ab равно композиции правых умножений: mulRight R (a b) = (mulRight R b) ∘ (mulRight R a).

LaTeX

$$$$ mulRight R (a b) = (mulRight R b) \circ (mulRight R a). $$$$

Lean4

@[simp]
theorem mulRight_mul [IsScalarTower R A A] (a b : A) : mulRight R (a * b) = (mulRight R b).comp (mulRight R a) :=
  by
  ext
  simp only [mulRight_apply, comp_apply, mul_assoc]

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