A real basis of integral lattice vectors gives a rational number-field basis. Its real coordinates on embedded field elements are the corresponding rational coordinates, so missing-span conditions transfer without any rationality assumption on a real linear relation.

theorem CCDN.exists_field_basis_of_euclidean_lattice_basis (K : Type u_1) [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℝ (NumberField.mixedEmbedding.euclidean.mixedSpace K)) (hb : ∀ (i : ι), b i ∈ NumberField.mixedEmbedding.euclidean.integerLattice K) : ∃ (v : ι → NumberField.RingOfIntegers K) (q : Module.Basis ι ℚ K), (∀ (i : ι), q i = ↑(v i)) ∧ ∀ (i : ι), (euclideanNumberFieldEmbedding K) (q i) = b i

A real basis b of the Euclidean mixed space consisting of vectors of the integer lattice comes from a ℚ-basis q of K consisting of algebraic integers v i, with euclideanNumberFieldEmbedding K (q i) = b i.

theorem CCDN.euclidean_notMem_basis_span_of_coordinate_ne_zero (K : Type u_1) [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℝ (NumberField.mixedEmbedding.euclidean.mixedSpace K)) (q : Module.Basis ι ℚ K) (hmap : ∀ (i : ι), (euclideanNumberFieldEmbedding K) (q i) = b i) {x : K} {i : ι} (hi : (q.repr x) i ≠ 0) {S : Set ι} (hiS : i ∉ S) : (euclideanNumberFieldEmbedding K) x ∉ Submodule.span ℝ (⇑b '' S)

If the real basis b is the image of the rational basis q and the i-th q-coordinate of x : K is nonzero, then the embedding of x does not lie in the real span of b '' S for any S not containing i.