coe_inv — Mathlib

English

For every real x, the inverse of its hyperreal image equals the hyperreal image of the inverse: (x^{*})^{-1} = (x^{-1})^{*}.

Русский

Обратная гиперреального образа числа равна образу гиперреального числа обратного: (x^{*})^{-1} = (x^{-1})^{*}.

LaTeX

$$$(x^{\\*})^{-1} = (x^{-1})^{\\*}$, \\text{for all } x \\neq 0$$$

Lean4

@[simp, norm_cast]
theorem coe_inv (x : ℝ) : ↑x⁻¹ = (x⁻¹ : ℝ*) :=
  rfl

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