Theorem NumberField.coe_discr

Modification history

2024-10-24 13:22
Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
chore: split NumberTheory/NumberField/Discriminant (#18168) …
Modified NumberField.coe_discrView on Github →
2023-09-01 13:27
Mathlib/NumberTheory/NumberField/Discriminant.lean
feat: define the discriminant of a number field (#6394) …
Added NumberField.coe_discrView on Github →