inv_natCast_num

Mathlib.Data.Rat.Lemmas

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

English

For any a ∈ ℕ, the numerator of (a : ℚ)⁻¹ equals Int.sign a.

Русский

Для любого a ∈ ℕ числитель (a : ℚ)⁻¹ равен Int.sign a.

LaTeX

$$$(a : \\mathbb{Q})^{-1}.num = \\operatorname{Int.sign}(a)$$$

Lean4

theorem inv_natCast_num (a : ℕ) : (a : ℚ)⁻¹.num = Int.sign a := by simp

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

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

Разделы

Аффилиация

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