commute_mulLeft_right — Mathlib

English

The nonunital left-multiplication homomorphism has compatible maps with mul and extensionality; it exhibits how left multiplication intertwines with the endomorphism structure.

Русский

Гомоморфизм левого умножения имеет согласованные отображения с mul и свойство различимости; демонстрирует как левое умножение сопряжено с структурой эдноморфизмов.

LaTeX

$$$$ \text{(map_mul', map_zero', ext_)} $$$$

Lean4

theorem commute_mulLeft_right (a b : A) : Commute (mulLeft R a) (mulRight R b) :=
  by
  ext c
  exact (mul_assoc a c b).symm

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