coe_inv — Mathlib

English

Embedding preserves inversion: the inverse of a scalar x embedded into the quaternions equals the quaternion inverse of the embedded x.

Русский

Вложение сохраняет обратное: обратное элементу x при вложении в кватернионы равно обратному кватерниону от вложенного x.

LaTeX

$$$x \in R \Rightarrow (x)^{-1} \text{ in } \mathbb{H}(R) = (x)^{-1}\text{ in } \mathbb{H}(R)$$$

Lean4

@[norm_cast, simp]
theorem coe_inv (x : R) : ((x⁻¹ : R) : ℍ[R]) = (↑x)⁻¹ :=
  map_inv₀ (algebraMap R ℍ[R]) _

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