inv_natCast_den

Mathlib.Data.Rat.Lemmas

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

English

For any a ∈ ℕ, the denominator of (a : ℚ)⁻¹ equals if a = 0 then 1 else a.

Русский

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

LaTeX

$$$((a : \\mathbb{Q})^{-1}.den) = \\begin{cases} 1, & a = 0 \\\\ a, & a > 0 \\end{cases}$$$

Lean4

theorem inv_natCast_den (a : ℕ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a := by simp

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

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

Разделы

Аффилиация

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