Theorem NumberField.mixedEmbedding.fundamentalCone.integralPoint_ne_zero

Modification history

2024-10-31 10:18
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
feat(NumberField/FundamentalCone): generalize the bijection to integral ideals (#18248) …
Deleted NumberField.mixedEmbedding.fundamentalCone.integralPoint_ne_zeroView on Github →
2024-10-01 05:27
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
chore: tidy various files (#17095)
Modified NumberField.mixedEmbedding.fundamentalCone.integralPoint_ne_zeroView 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.integralPoint_ne_zeroView on Github →