commute_rmul_rmul_sq

Mathlib.Algebra.Jordan.Basic

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

English

Right multiplications by a and a^2 commute.

Русский

Правая умножение на a и на a^2 commute.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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