instFloorSemiringNat — Mathlib

English

The integers ℤ form a FloorRing with floor and ceil given by the identity function.

Русский

Целые числа ℤ образуют FloorRing, у которого floor и ceil совпадают с тождественной отображением.

LaTeX

$$$\text{FloorRing } \mathbb{Z} \text{ with } \text{floor} = \text{id},\ \text{ceil} = \text{id}$$$

Lean4

instance : FloorSemiring ℕ where
  floor := id
  ceil := id
  floor_of_neg ha := (Nat.not_lt_zero _ ha).elim
  gc_floor _ := by rw [Nat.cast_id, id_def]
  gc_ceil n a := by rw [Nat.cast_id, id_def]

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