English
For every rational number x, the natural value of its positive-denominator part equals its standard denominator. In reduced form x = a/b with b > 0, the positive-denominator of x corresponds to b, so (x.pnatDen) as a natural equals x.den.
Русский
Для любого рационального числа x его положительный знаменатель (в виде натурального числа) совпадает с обычным знаменателем x. Пусть x = a/b в сокращённой форме, b > 0, тогда (x.pnatDen) = b и x.den = b.
LaTeX
$$$ (x \mathrm{.pnatDen} : \mathbb{N}) = x \mathrm{.den} \quad \text{for } x \in \mathbb{Q} $$$
Lean4
@[simp]
theorem coe_pnatDen (x : ℚ) : (x.pnatDen : ℕ) = x.den :=
rfl
