mem_span_integralBasis — Mathlib

English

An element x ∈ K lies in the ℤ-span of the integralBasis if and only if x is in the image of the algebra map from 𝓞K to K.

Русский

Элемент x ∈ K лежит в ℤ-замкнутом спане интегрального базиса тогда и только тогда, когда x лежит в образе алгебраической карты от 𝓞K в K.

LaTeX

$$$x \\in \\operatorname{span}_{\\mathbb{Z}}(\\operatorname{range}(integralBasis K)) \\iff x \\in \\operatorname{range}(\\text{algebraMap}(\\mathcal{O}_K \\to K)).$$$

Lean4

theorem mem_span_integralBasis {x : K} :
    x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ (algebraMap (𝓞 K) K).range := by
  rw [integralBasis, Basis.localizationLocalization_span, LinearMap.mem_range, IsScalarTower.coe_toAlgHom',
    RingHom.mem_range]

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