Theorem NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply

Modification history

2024-10-31 10:18
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
feat(NumberField/FundamentalCone): generalize the bijection to integral ideals (#18248) …
Added NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_applyView on Github →