Commit 2025-05-27 08:57 dff1ecda

View on Github →

chore: tidy various files (#25212)

Estimated changes

Modified Mathlib/CategoryTheory/Equivalence/Symmetry.lean

Modified Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean

Modified Mathlib/Data/Int/Cast/Basic.lean

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

modified theorem SubMulAction.compl_def

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean

Modified Mathlib/Order/Hom/Order.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean

modified theorem UniqueFactorizationMonoid.dvd_of_normalized_factor

Modified Mathlib/Topology/MetricSpace/GromovHausdorff.lean