English
The fundamental domain of the ℤ-lattice spanned by a basis b is the set of elements m ∈ E such that for every i, the i-th coordinate repr m i lies in the half-open interval [0,1).
Русский
Фундаментальная область ℤ-решетки, порождаемая базисом b, состоит из элементов m ∈ E, для которых во всех координатах i коэффициент repr m i лежит в интервале [0,1).
LaTeX
$$$\\text{fundamentalDomain}(b) = \\{\,m \\in E : \\forall i, \\; b.repr\\,m\\,i \\in [0,1) \\,\\}$$$
Lean4
theorem smul {c : K} (hc : c ≠ 0) : c • span ℤ (Set.range b) = span ℤ (Set.range (b.isUnitSMul (fun _ ↦ hc.isUnit))) :=
by
rw [smul_span, Set.smul_set_range]
congr!
rw [Basis.isUnitSMul_apply]
