Commit 2025-07-25 21:58 208559cf

View on Github →

chore: fix more indentation (#27491) Found by the linter in #27473.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

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

modified theorem CommMonCat.hom_ofHom

modified theorem MonCat.hom_ofHom

Modified Mathlib/Algebra/Category/Semigrp/Basic.lean

modified theorem MagmaCat.hom_ofHom

Modified Mathlib/Algebra/Group/Even.lean

Modified Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

Modified Mathlib/Algebra/Group/Subgroup/Defs.lean

Modified Mathlib/Algebra/GroupWithZero/Action/Pointwise/Set.lean

Modified Mathlib/Algebra/Module/Defs.lean

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

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

Modified Mathlib/Algebra/Order/AddTorsor.lean

Modified Mathlib/Algebra/Order/SuccPred/TypeTags.lean

modified theorem Order.pred_toMul

Modified Mathlib/CategoryTheory/Category/Preorder.lean

Modified Mathlib/CategoryTheory/ComposableArrows.lean

modified theorem CategoryTheory.ComposableArrows.map'_self

Modified Mathlib/CategoryTheory/Core.lean

Modified Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Preorder/PrincipalSeg.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Composition.lean

Modified Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean

modified theorem CategoryTheory.ObjectProperty.FullSubcategory.map_inclusion

Modified Mathlib/CategoryTheory/PathCategory/Basic.lean

Modified Mathlib/CategoryTheory/Quotient.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/Data/ZMod/IntUnitsPower.lean

modified theorem toMul_uzpow

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

modified theorem SubMulAction.compl_def

Modified Mathlib/GroupTheory/OreLocalization/Basic.lean

Modified Mathlib/Logic/Basic.lean

modified theorem imp_forall_iff_forall

Modified Mathlib/Order/Category/PartOrd.lean

modified theorem PartOrd.hom_ofHom

modified theorem PartOrd.ofHom_hom

Modified Mathlib/Order/Category/Preord.lean

modified theorem Preord.hom_ofHom

modified theorem Preord.ofHom_hom

Modified Mathlib/Order/Filter/Ultrafilter/Defs.lean

Modified Mathlib/Order/Hom/Order.lean

Modified Mathlib/RingTheory/PolynomialLaw/Basic.lean

Modified Mathlib/Tactic/NormNum/Prime.lean