inv_natCast_den_of_pos

Mathlib.Data.Rat.Lemmas

URI: https://scilib.ai/kg/mathlib#Rat.inv_natCast_den_of_pos

← MathLib Explorer

English

For any a ∈ ℕ with a > 0, the denominator of (a : ℚ)⁻¹ equals a, i.e., the same as the natural number.

Русский

Для любого a ∈ ℕ, a > 0, знаменатель (a : ℚ)⁻¹ равен a.

LaTeX

$$$((a : \\mathbb{Q})^{-1}.den) = a$$$

Lean4

theorem inv_natCast_den_of_pos {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.den = a :=
  by
  rw [← Int.ofNat_inj, ← Int.cast_natCast a, inv_intCast_den_of_pos]
  rwa [Int.natCast_pos]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru