inv_intCast_num_of_pos

Mathlib.Data.Rat.Lemmas

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

English

For any a ∈ ℤ with a > 0, the numerator of (a : ℚ)⁻¹ equals Int.sign a, i.e., 1.

Русский

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

LaTeX

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

Lean4

theorem inv_intCast_num_of_pos {a : ℤ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 := by simp [*]

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

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

Разделы

Аффилиация

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