imK_star — Mathlib

English

Let a be a quaternion over a commutative ring R. Then the K-component of the conjugate equals the negation of the original K-component: (star a).imK = - a.imK.

Русский

Пусть a — кватернион над кольцом R. Тогда K-компонента сопряжения равна противоположной исходной K-компоненте: (star a).imK = - a.imK.

LaTeX

$$$ (star a).imK = - a.imK $$$

Lean4

@[simp]
theorem imK_star : (star a).imK = -a.imK :=
  rfl

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