fract_eq_self — Mathlib

English

Two vectors have the same fract part with respect to b iff their difference lies in the integer-span of b.

Русский

Разности двух векторов принадлежат spanℤ(range(b)) тогда и только тогда, когда их дробные части совпадают.

LaTeX

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

Lean4

theorem fract_eq_self {x : E} : fract b x = x ↔ x ∈ fundamentalDomain b := by
  classical simp only [Basis.ext_elem_iff b, repr_fract_apply, Int.fract_eq_self, mem_fundamentalDomain, Set.mem_Ico]

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