mem_rat_span_latticeBasis — Mathlib

English

The coordinate representation of the canonical embedding applied to the integral basis matches the coordinate representation of the integral basis itself; i.e., the reprs correspond under the embedding.

Русский

Координатное представление канонического вложения применённого к интегральному базису совпадает с представлением интегрального базиса.

LaTeX

$$$\\mathrm{(latticeBasis(K)).repr}(\\mathrm{canonicalEmbedding}(K)\\,x)=\\mathrm{integralBasis}(K).\\mathrm{repr}(x)$$$

Lean4

theorem mem_rat_span_latticeBasis [NumberField K] (x : K) :
    canonicalEmbedding 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

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