English
A rational-span statement: membership in span of latticeBasis corresponds to membership in the image of the integral basis under mixedEmbedding.
Русский
Утверждение о включении по рациональному базису: принадлежность к span базиса решётки эквивалентна принадлежности к образу интегрального базиса через смешанное вложение.
LaTeX
$$$ x \in Submodule.span \mathbb{Z} (Set.range (latticeBasis K)) $$$
Lean4
theorem mem_rat_span_latticeBasis (x : K) : mixedEmbedding K x ∈ Submodule.span ℚ (Set.range (latticeBasis K)) :=
by
rw [← Basis.sum_repr (integralBasis K) x, map_sum]
simp_rw [map_rat_smul]
refine Submodule.sum_smul_mem _ _ (fun i _ ↦ Submodule.subset_span ?_)
rw [← latticeBasis_apply]
exact Set.mem_range_self i