fract — Mathlib

English

For a lattice basis b in a normed space, fract(m) is the fractional part of m with respect to b, i.e., fract(m) = m − floor_b(m).

Русский

Для базиса решётки b в нормированном пространстве fract(m) — это дробная часть в отношении к b, то есть fract(m) = m − floor_b(m).

LaTeX

$$$\\text{fract}_b(m) = m - \\lfloor b \\rfloor_m$$$

Lean4

/-- The map that sends a vector `E` to the `fundamentalDomain` of the lattice,
see `ZSpan.fract_mem_fundamentalDomain`, and `fractRestrict` for the map with the codomain
restricted to `fundamentalDomain`. -/
def fract (m : E) : E :=
  m - floor b m

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