isInt_intFloor — Mathlib

English

Let R be a ring with a linear order, an IsStrictOrderedRing, and a FloorRing. If r is an integer m, then ⌊r⌋ is also an integer m; i.e. IsInt r m → IsInt ⌊r⌋ m.

Русский

Пусть R — кольцо с линейным порядком, IsStrictOrderedRing и FloorRing. Если r целое число m, то ⌊r⌋ тоже целое m; то есть IsInt r m → IsInt ⌊r⌋ m.

LaTeX

$$$$ \\text{IsInt } r\, m \\rightarrow \\text{IsInt } \\lfloor r \\rfloor\, m, \\quad r \\in R,\\; m \\in \\mathbb{Z}. $$$$

Lean4

theorem isInt_intFloor {R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : ℤ) :
    IsInt r m → IsInt ⌊r⌋ m := by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

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