Theorem NumberField.abs_discr_ge'

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_ge'View on Github →