imI_neg — Mathlib

English

The i-coordinate of the negative quaternion is the negation of the i-coordinate of the quaternion: ImI(-a) = -ImI(a).

Русский

Коэффициент при i в отрицательном кватернионе равен минусу соответствующего коэффициента: ImI(-a) = -ImI(a).

LaTeX

$$$$\forall a \in \mathbb{H}(R):\ \operatorname{Im}_I(-a) = -\operatorname{Im}_I(a).$$$$

Lean4

@[simp]
theorem imI_neg : (-a).imI = -a.imI :=
  rfl

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