canLift — Mathlib

English

If a rational q has denominator 1, then q is representable as an integer, i.e., q = (n : ℚ) for some n ∈ ℤ.

Русский

Если q имеет знаменатель 1, то q равняется некоторому целому, т.е. q = (n : ℚ) для некоторого n ∈ ℤ.

LaTeX

$$$q.den = 1 \Rightarrow \exists n \in \mathbb{Z}, q = (n : \mathbb{Q})$$$

Lean4

instance canLift : CanLift ℚ ℤ (↑) fun q => q.den = 1 :=
  ⟨fun q hq => ⟨q.num, coe_int_num_of_den_eq_one hq⟩⟩
    -- Will be subsumed by `Int.coe_inj` after we have defined
    -- `LinearOrderedField ℚ` (which implies characteristic zero).

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