eq_re_iff_mem_range_coe — Mathlib

English

A quaternion a satisfies a = a.re if and only if a lies in the range of the real embedding into quaternions.

Русский

Кватернион удовлетворяющий a = a.re эквивалентен тому, что он лежит в диапазоне отображения вещественных чисел в кватернионы.

LaTeX

$$$ a = a.re \iff a \in \mathrm{range}(\mathrm{coe} : \mathbb{R} \to \mathbb{H}(R)) $$$

Lean4

theorem eq_re_iff_mem_range_coe {a : ℍ[R]} : a = a.re ↔ a ∈ Set.range (coe : R → ℍ[R]) :=
  QuaternionAlgebra.eq_re_iff_mem_range_coe

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