Commit 2026-01-30 12:44 000c398e

View on Github →

chore: tidy various files (#34610)

Estimated changes

Modified Archive/Examples/Kuratowski.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Directed.lean

modified theorem Subalgebra.coe_iSup_of_directed

Modified Mathlib/Algebra/Group/Irreducible/Indecomposable.lean

Modified Mathlib/Algebra/Module/FinitePresentation.lean

Modified Mathlib/Algebra/Module/Torsion/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/Coalgebra.lean

Modified Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

Modified Mathlib/Analysis/Meromorphic/Basic.lean

Modified Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

Modified Mathlib/CategoryTheory/Abelian/Injective/Extend.lean

Modified Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean

Modified Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

Modified Mathlib/Combinatorics/SimpleGraph/Diam.lean

Modified Mathlib/Combinatorics/SimpleGraph/Metric.lean

Modified Mathlib/Geometry/Euclidean/NinePointCircle.lean

Modified Mathlib/GroupTheory/OreLocalization/Basic.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

Modified Mathlib/LinearAlgebra/Transvection.lean

Modified Mathlib/MeasureTheory/Measure/AddContent.lean

Modified Mathlib/ModelTheory/Topology/Types.lean

Modified Mathlib/ModelTheory/Types.lean

modified theorem FirstOrder.Language.Theory.CompleteType.typesWith_top

Modified Mathlib/NumberTheory/Fermat.lean

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

Modified Mathlib/RepresentationTheory/Subrepresentation.lean

Modified Mathlib/RingTheory/Coalgebra/Basic.lean

Modified Mathlib/RingTheory/KrullDimension/Regular.lean

Modified Mathlib/RingTheory/Morita/Matrix.lean

Modified Mathlib/RingTheory/MvPowerSeries/Expand.lean

Modified Mathlib/RingTheory/PicardGroup.lean

Modified Mathlib/RingTheory/PowerSeries/Expand.lean

Modified Mathlib/Topology/Algebra/MulAction.lean

Modified Mathlib/Topology/OpenPartialHomeomorph/Defs.lean