Theorem NumberField.mixedEmbedding.span_latticeBasis

Modification history

2024-09-20 12:33
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
feat(NumberField/CanonicalEmbedding/FundamentalCone): Define the subset of integral points (#16921) …
Added NumberField.mixedEmbedding.span_latticeBasisView on Github →