commute_lmul_rmul_sq

Mathlib.Algebra.Jordan.Basic

URI: https://scilib.ai/kg/mathlib#commute_lmul_rmul_sq

English

The left multiplication by a commutes with the right multiplication by a^2.

Русский

Левое умножение на a коммутирует с правым умножением на a^2.

LaTeX

$$Commute (L a) (R (a^2))$$

Lean4

@[simp]
theorem commute_lmul_rmul_sq (a : A) : Commute (L a) (R (a * a)) :=
  AddMonoidHom.ext fun _ => (IsJordan.lmul_comm_rmul_rmul _ _).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru