floor — Mathlib

English

The floor function on a general ordered ring assigns to a ∈ α the greatest natural number not exceeding a, i.e. ⌊a⌋₊.

Русский

Округление вниз в общем упорядоченном кольце задаёт на элементе a наибольшее натуральное число, не превосходящее a, то есть ⌊a⌋₊.

LaTeX

$$$\text{floor}:\alpha \to \mathbb{N} \text{ is the FloorSemiring.floor function.}$$$

Lean4

/-- `⌊a⌋₊` is the greatest natural `n` such that `n ≤ a`. If `a` is negative, then `⌊a⌋₊ = 0`. -/
def floor : α → ℕ :=
  FloorSemiring.floor

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