cast_inv — Mathlib

English

For p ∈ ℚ≥0, the image of its inverse under the embedding equals the inverse of its image in α: (p⁻¹ : ℚ≥0) = (p : α)⁻¹.

Русский

Пусть p ∈ ℚ≥0. Образ его обратного через отображение равен обратному образу самого элемента в α: (p⁻¹ : ℚ≥0) = (p : α)⁻¹.

LaTeX

$$$ (p^{-1} : \alpha) = (p : \alpha)^{-1} $$$

Lean4

@[simp, norm_cast]
theorem cast_inv (p) : (p⁻¹ : ℚ≥0) = (p : α)⁻¹ :=
  map_inv₀ (castHom α) _

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