pnatDen

Mathlib.Data.Rat.Lemmas

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

English

Denominator as a positive natural: pnatDen(x) = ⟨x.den, x.pos⟩ for x ∈ ℚ.

Русский

Знаменатель как положительное натуральное число: pnatDen(x) = ⟨x.den, x.pos⟩ для x ∈ ℚ.

LaTeX

$$$\\text{pnatDen}(x) = \\langle x.den, x.pos \\rangle$$$

Lean4

/-- Denominator as `ℕ+`. -/
def pnatDen (x : ℚ) : ℕ+ :=
  ⟨x.den, x.pos⟩

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

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

Разделы

Аффилиация

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