ofReal_inv — Mathlib

English

For any real number r, its image in K satisfies the relation ((r⁻¹ : ℝ) : K) = (r : K)⁻¹, i.e., inversion commutes with the real embedding.

Русский

Для любого r ∈ ℝ образ r в K удовлетворяет ((r⁻¹ : ℝ) : K) = (r : K)⁻¹; обратное сохраняется под вложением из ℝ.

LaTeX

$$$$ ((r^{-1} : \mathbb{R}) : K) = (r : K)^{-1}. $$$$

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_inv (r : ℝ) : ((r⁻¹ : ℝ) : K) = (r : K)⁻¹ :=
  map_inv₀ _ r

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