Theorem NumberField.mixedEmbedding.fundamentalCone.exists_unique_preimage_of_mem_integerSet

Modification history

2024-12-18 19:47
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
chore(Logic/ExistsUnique): amend usages of existsUnique to follow naming convention (#20028) …
Deleted NumberField.mixedEmbedding.fundamentalCone.exists_unique_preimage_of_mem_integerSetView on Github →
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.exists_unique_preimage_of_mem_integerSetView on Github →