Theorem NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis

Modification history

2024-04-05 07:05

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

chore: split `NumberTheory.NumberField.CanonicalEmbedding` (#11873) …

Modified NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis View on Github →

2024-02-07 19:45

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

feat: Generalize results of `CanonicalEmbedding` to fractional ideals (#9837) …

Added NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis View on Github →