Theorem NumberField.linearDisjoint_of_isGalois_isCoprime_discr

Modification history

2025-11-12 21:15
Mathlib/NumberTheory/NumberField/Discriminant/Different.lean
feat(NumberField): discriminant in disjoint extensions (#29943) …
Added NumberField.linearDisjoint_of_isGalois_isCoprime_discrView on Github →