Commit 2024-04-02 13:53 921bb500

View on Github →

fix: align Int.norm_eq_abs with its mathlib3 meaning (#11841)

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Basic.lean

modified theorem Int.norm_eq_abs

Modified Mathlib/Analysis/NormedSpace/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean