commute_lmul_sq_rmul

Mathlib.Algebra.Jordan.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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