inv_intCast_num

Mathlib.Data.Rat.Lemmas

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

English

For any integer a, the numerator of (a : ℚ)⁻¹ is Int.sign a.

Русский

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

LaTeX

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

Lean4

theorem inv_intCast_num (a : ℤ) : (a : ℚ)⁻¹.num = Int.sign a := by simp

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

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

Разделы

Аффилиация

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