Commit 2024-02-14 07:40 7a64c731

View on Github →

chore: Some constants in CanonicalEmbedding should be NNReal and not ENNReal (#10032)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

deleted theorem NumberField.mixedEmbedding.convexBodyLTFactor_lt_top

added theorem NumberField.mixedEmbedding.convexBodyLTFactor_ne_zero

deleted theorem NumberField.mixedEmbedding.convexBodyLTFactor_pos

deleted theorem NumberField.mixedEmbedding.convexBodySumFactor_ne_top

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

Modified Mathlib/NumberTheory/NumberField/Units.lean