star_eq_self — Mathlib

English

Under suitable assumptions, star a = a if and only if a is real (a = a.re).

Русский

При подходящих предположениях star a = a тогда и только тогда, когда a вещественный (a = a.re).

LaTeX

$$$\star a = a \iff a = a.re$$$

Lean4

@[simp]
theorem star_eq_self {c₁ c₂ : R} {a : ℍ[R,c₁,c₂,c₃]} : star a = a ↔ a = a.re := by
  simp_all [QuaternionAlgebra.ext_iff, neg_eq_iff_add_eq_zero, add_self_eq_zero]

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