cast_inv_nat — Mathlib

English

For natural n, the inverse of n in ℚ, cast to α, equals the inverse of n in α.

Русский

Для натурального n обратное к n в ℚ, приведённое в α, равно обратному к n в α.

LaTeX

$$$\forall n \in \mathbb{N},\ ↑(n^{-1}) = (n)^{-1}.$$$

Lean4

@[simp]
theorem cast_inv_nat (n : ℕ) : ((n⁻¹ : ℚ) : α) = (n : α)⁻¹ :=
  by
  rcases n with - | n
  · simp
  rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero, Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n),
    Int.cast_one, one_div]

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