coe_inv — Mathlib

English

Coercion commutes with inverse: the real value of the inverse in NNReal equals the real inverse.

Русский

Коэрцирование сохраняет обратное: действительное значение обратного в NNReal равно действительному обратному.

LaTeX

$$$ ((r^{-1} : \mathbb{R}_{\ge 0}) : \mathbb{R}) = r^{-1} $$$

Lean4

@[simp, norm_cast]
protected theorem coe_inv (r : ℝ≥0) : ((r⁻¹ : ℝ≥0) : ℝ) = (r : ℝ)⁻¹ :=
  rfl

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