English
The floor map sends a vector m in E to the element of the ℤ-lattice spanned by b obtained by taking the floor of each coordinate with respect to b.
Русский
Оценка по целым числам отправляет вектор m ∈ E в элемент ℤ-решетки, порожденной b, где каждая координата по базису b взята округлением вниз.
LaTeX
$$$ \operatorname{floor}_b(m) = \sum_i \Big\lfloor b.repr(m)_i \Big\rfloor \; b.restrictScalars\mathbb{Z}_i $$$
Lean4
/-- The map that sends a vector of `E` to the element of the ℤ-lattice spanned by `b` obtained
by rounding down its coordinates on the basis `b`. -/
def floor (m : E) : span ℤ (Set.range b) :=
∑ i, ⌊b.repr m i⌋ • b.restrictScalars ℤ i
