Theorems · Definition · ring theory

QuaternionAlgebra.im

{R : Type u_3} → {c₁ c₂ c₃ : R} → [Zero R] → QuaternionAlgebra R c₁ c₂ c₃ → QuaternionAlgebra R c₁ c₂ c₃

The imaginary part of a quaternion. Note that unless c₂ = 0, this definition is not particularly well-behaved; for instance, QuaternionAlgebra.star_im only says that the star of an imaginary quaternion is imaginary under this condition.

Defined in

Mathlib.Algebra.Quaternion

Cited by

20 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

Zero