instInv — Mathlib

English

The quaternion algebra carries a division operation: the inverse of a quaternion a is given by (normSq a)^{-1} times the conjugate of a.

Русский

Кватернионная алгебра обладает делением: обратный элемент кватерниона a равен (normSq a)^{-1} умножить на сопряжённый a.

LaTeX

$$$a^{-1} = (\|a\|^2)^{-1} \cdot \overline{a}$$$

Lean4

@[simps -isSimp]
instance instInv : Inv ℍ[R] :=
  ⟨fun a => (normSq a)⁻¹ • star a⟩

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