English
Let R be a ring with linear order, IsStrictOrderedRing, and FloorRing. If r is a positive rational represented by n/d (IsNNRat r n d), then the floor of r is a natural number equal to n/d, i.e. IsNat ⌊r⌋ (n/d).
Русский
Пусть R — кольцо с линейным порядком, IsStrictOrderedRing и FloorRing. Если r положительная рациональная с записью r = n/d (IsNNRat r n d), то ⌊r⌋ является натуральным числом, равным n/d.
LaTeX
$$$$ \\text{IsNNRat } r\, n\, d \\rightarrow \\text{IsNat } \\lfloor r \\rfloor \\, (n/d). $$$$
Lean4
theorem isNat_intFloor_ofIsNNRat (r : α) (n : ℕ) (d : ℕ) : IsNNRat r n d → IsNat ⌊r⌋ (n / d) :=
by
rintro ⟨inv, rfl⟩
constructor
simp only [invOf_eq_inv, ← div_eq_mul_inv]
rw [← Int.ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d, ← floor_cast (α := α), Rat.cast_div, cast_natCast,
cast_natCast]
