Theorem NumberField.isCoprime_differentIdeal_of_isCoprime_discr

Modification history

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