cast_inv_of_ne_zero — Mathlib

English

If q.num ≠ 0 in α, then the inverse commutes with the cast: (q⁻¹ : ℚ≥0) = (q)⁻¹ in α.

Русский

Если q.num ≠ 0 в α, то обратный элемент сохраняется под вложением: (q⁻¹ : ℚ≥0) = q⁻¹ в α.

LaTeX

$$$ (q^{-1} : \mathbb{Q}_{\ge 0}) = (q : \alpha)^{-1} $$$

Lean4

@[norm_cast]
theorem cast_inv_of_ne_zero (hq : (q.num : α) ≠ 0) : (q⁻¹ : ℚ≥0) = (q⁻¹ : α) := by
  rw [inv_def, cast_divNat_of_ne_zero _ hq, cast_def, inv_div]

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