cast_inv_int — Mathlib

English

Let α be a division ring. For every integer n, the image of n^{-1} in ℚ cast to α equals the inverse of n cast to α.

Русский

Пусть α — кольцо деления. Для любого целого n образ n^{-1} из ℚ, приведённый в α, равен обратному образу n в α.

LaTeX

$$$ ∀ \alpha [\mathrm{DivisionRing}\,\alpha], ∀ n : \mathbb{Z}, \left( (n^{-1} : \mathbb{Q}) : \alpha \right) = (n : \alpha)^{-1}. $$$

Lean4

@[simp]
theorem cast_inv_int (n : ℤ) : ((n⁻¹ : ℚ) : α) = (n : α)⁻¹ :=
  by
  rcases n with n | n
  · simp [cast_inv_nat]
  · simp only [Int.cast_negSucc, cast_neg, inv_neg, cast_inv_nat]

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