Commit 2023-12-15 10:22 5ab70216

View on Github →

chore: golf and generalize discr_eq_discr_of_algEquiv (#9068)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

Modified Mathlib/RingTheory/Discriminant.lean

modified theorem Algebra.discr_eq_discr_of_algEquiv