Commit 2025-07-22 20:14 eed082b5

View on Github →

chore: tidy various files (#27356)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

Modified Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

Modified Mathlib/Algebra/Exact.lean

Modified Mathlib/Algebra/GroupWithZero/Equiv.lean

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Integral.lean

Modified Mathlib/Analysis/Complex/IntegerCompl.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/Laplacian.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

Modified Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

Modified Mathlib/Combinatorics/Configuration.lean

Modified Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean

Modified Mathlib/FieldTheory/Normal/Closure.lean

Modified Mathlib/FieldTheory/RatFunc/AsPolynomial.lean

modified theorem Polynomial.valuation_aeval_monomial_eq_valuation_pow

Modified Mathlib/Geometry/Euclidean/MongePoint.lean

Modified Mathlib/GroupTheory/FreeAbelianGroup.lean

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

Modified Mathlib/LinearAlgebra/Span/Basic.lean

Modified Mathlib/Logic/Function/Iterate.lean

Modified Mathlib/Order/Fin/Basic.lean

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/Shapiro.lean

Modified Mathlib/RepresentationTheory/Induced.lean

Modified Mathlib/RingTheory/Filtration.lean