mem_rat_span_latticeBasis — Mathlib

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

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