Commit 2025-04-16 08:54 1a64c90d

View on Github →

feat(NumberField/Discriminant): better lower bound for totally complex number fields (#24076)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean

added theorem NumberField.abs_discr_ge'

added theorem NumberField.abs_discr_ge_of_isTotallyComplex

added theorem NumberField.abs_discr_rpow_ge_of_isTotallyComplex

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

added theorem NumberField.IsTotallyComplex.nrRealPlaces_eq_zero

added theorem NumberField.IsTotallyReal.nrComplexPlaces_eq_zero

added theorem NumberField.nrComplexPlaces_eq_zero_iff

added theorem NumberField.nrRealPlaces_eq_zero_iff