Def NumberField.mixedEmbedding.fundamentalCone.intNorm

Modification history

2024-10-31 10:18

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

feat(NumberField/FundamentalCone): generalize the bijection to integral ideals (#18248) …

Modified NumberField.mixedEmbedding.fundamentalCone.intNorm View on Github →

2024-09-20 12:33

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

feat(NumberField/CanonicalEmbedding/FundamentalCone): Define the subset of integral points (#16921) …

Added NumberField.mixedEmbedding.fundamentalCone.intNorm View on Github →