mulLeft_mul — Mathlib

English

Left multiplication by ab equals the composition of left multiplications by a and then by b: mulLeft R (a b) = (mulLeft R a) ∘ (mulLeft R b).

Русский

Умножение слева на произведение ab равно композиции умножения слева по a, затем по b: mulLeft R (a b) = (mulLeft R a) ∘ (mulLeft R b).

LaTeX

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

Lean4

@[simp]
theorem mulLeft_mul [SMulCommClass R A A] (a b : A) : mulLeft R (a * b) = (mulLeft R a).comp (mulLeft R b) :=
  by
  ext
  simp only [mulLeft_apply, comp_apply, mul_assoc]

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