Commit 2024-08-12 15:39 d6d9c226

View on Github →

chore: remove unnecessary root qualifications (#15704)

Estimated changes

Modified Mathlib/Algebra/Group/Equiv/Basic.lean

Modified Mathlib/Data/NNReal/Basic.lean

Modified Mathlib/NumberTheory/KummerDedekind.lean

Modified Mathlib/RingTheory/Algebraic.lean

Modified Mathlib/RingTheory/ClassGroup.lean

Modified Mathlib/RingTheory/Ideal/Norm.lean

modified theorem Ideal.absNorm_top

Modified Mathlib/RingTheory/Kaehler/Basic.lean

Modified Mathlib/RingTheory/Localization/Submodule.lean

Modified Mathlib/RingTheory/MvPolynomial/Localization.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

Modified Mathlib/RingTheory/TensorProduct/Basic.lean