coe_inv — Mathlib

English

The inverse operation on the unit sphere corresponds to the ordinary inverse in the base ring: the coercion commutes with inversion.

Русский

Операция обратного элемента на единичной сфере соответствует обычному обратному в базовом кольце: приведение по коэфициенту сохраняет инверсию.

LaTeX

$$$x \mapsto x^{-1} \Rightarrow \uparrow x^{-1} = (\uparrow x)^{-1}$$$

Lean4

@[simp, norm_cast]
theorem coe_inv [NormedDivisionRing 𝕜] (x : sphere (0 : 𝕜) 1) : ↑x⁻¹ = (x⁻¹ : 𝕜) :=
  rfl

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