Commit 2023-08-02 09:22 6538bed2

View on Github →

feat(NumberTheory.NumberField.Basic): add mem_span_integralBasis (#5996) Add the following result:

theorem mem_span_integralBasis {x : K} :
    x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ 𝓞 K

that is, integralBasis is indeed a ℤ-basis of the ring of integers.

Estimated changes

modified theorem Submodule.map_span
modified theorem Submodule.map_span_le
modified theorem Submodule.span_image
modified theorem Submodule.span_preimage_le