Theorem NumberField.abs_discr_rpow_ge_of_isTotallyComplex

Modification history

2025-04-16 08:54
Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
feat(NumberField/Discriminant): better lower bound for totally complex number fields (#24076)
Added NumberField.abs_discr_rpow_ge_of_isTotallyComplexView on Github →