mul_star_eq_coe

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#QuaternionAlgebra.mul_star_eq_coe

English

Symmetrically, a · star a has real part equal to itself: a · star a = (a · star a).re.

Русский

Аналогично, произведение a на star a имеет вещественную часть, равную itself: a · star a = (a · star a).re.

LaTeX

$$$a \cdot \star a = (a \cdot \star a).re$$$

Lean4

theorem mul_star_eq_coe : a * star a = (a * star a).re :=
  by
  rw [← star_comm_self']
  exact a.star_mul_eq_coe

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

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

Разделы

Аффилиация

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