instModuleFree_of_discrete_submodule

English

Let E be a finite-dimensional real vector space and L a discrete ℤ-submodule (lattice) of E. Then L is a free ℤ-module (i.e., there exists a ℤ-basis of L).

Русский

Пусть E — конечномерное вещественное векторное пространство, и L — дискретная ℤ-подмодуль (решетка) в E. Тогда L является свободным ℤ-модулем (то есть существует ℤ-база для L).

LaTeX

$$$\\exists \\iota \\; (b : \\text{Basis } \\iota \\mathbb{Z} L)$$$

Lean4

instance instModuleFree_of_discrete_submodule {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology L] : Module.Free ℤ L :=
  by
  have : Module ℚ E := Module.compHom E (algebraMap ℚ ℝ)
  infer_instance

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