IntegerFloor

The greatest integer at or below x, in a floor ring.

IntegerFloor(x)The greatest integer at or below x, in a floor ring.

Typed signatures

Type	Package	Applies
(any) -> unknown	structures	always

Domain: Structures

Details

• The FloorRing protocol's member (Mathlib's Int.floor), and what Floor answers for such a type.
• The right adjoint of the integers' inclusion: an integer $n$ is at most $x$ exactly when $n \le \mathrm{IntegerFloor}(x)$.

Examples

Basic #

$\lfloor -2.5 \rfloor = -3$

live ↗

In$\mathrm{IntegerFloor}(-2.5)$Out$-3$

$\lfloor 7/2 \rfloor = 3$

live ↗

In$\mathrm{IntegerFloor}(\frac{7}{2})$Out$3$

About

Examples	2
Checked against	Wolfram Language 2 agree

Implementation

mappedwolframpackages/oracle/src/mappings.ts

See also: IntegerCeil, Floor, LowerTick