pnatDen_eq_iff_den_eq — Mathlib

English

Let x be a rational number and n a positive natural number. Then x.pnatDen = n holds iff x.den = ↑n, i.e., the positive-denominator equals n exactly when the ordinary denominator equals the natural value of n.

Русский

Пусть x ∈ ℚ и n ∈ ℕ_{>0}. Тогда x.pnatDen = n эквивалентно x.den = ↑n.

LaTeX

$$$ x.\mathrm{pnatDen} = n \iff x.\mathrm{den} = \uparrow n $$$

Lean4

theorem pnatDen_eq_iff_den_eq {x : ℚ} {n : ℕ+} : x.pnatDen = n ↔ x.den = ↑n :=
  Subtype.ext_iff

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