fract_mem_fundamentalDomain — Mathlib

English

Fract parts are equal iff the integer parts of coordinates align as in a lattice equivalence.

Русский

Дробные части равны тогда и только тогда, когда целые части координат согласованы согласно эквивалентности по решетке.

LaTeX

$$$ \operatorname{fract}_b(m) = \operatorname{fract}_b(n) \iff -m + n \in \operatorname{span}_{\mathbb{Z}}(\operatorname{range}(b)) $$$

Lean4

theorem fract_mem_fundamentalDomain (x : E) : fract b x ∈ fundamentalDomain b :=
  fract_eq_self.mp (fract_fract b _)

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