Commit 2025-05-14 18:08 5ffbd436

View on Github →

style: fix more doc-strings with indentation by an odd number of spaces (#24907) Continuation of #24893.

Estimated changes

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

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

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

Modified Mathlib/Algebra/GroupWithZero/Divisibility.lean

Modified Mathlib/Algebra/Module/LinearMap/End.lean

Modified Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

Modified Mathlib/Algebra/MvPolynomial/Rename.lean

Modified Mathlib/Algebra/Squarefree/Basic.lean

Modified Mathlib/Algebra/Star/Basic.lean

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

Modified Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

Modified Mathlib/Analysis/Complex/Hadamard.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/Normed/Lp/lpSpace.lean

Modified Mathlib/Analysis/Normed/Module/Dual.lean

Modified Mathlib/Analysis/Normed/Ring/WithAbs.lean

Modified Mathlib/Analysis/RCLike/BoundedContinuous.lean

Modified Mathlib/Analysis/SpecialFunctions/Stirling.lean

Modified Mathlib/CategoryTheory/Action.lean

Modified Mathlib/CategoryTheory/CodiscreteCategory.lean

Modified Mathlib/CategoryTheory/Enriched/Opposite.lean

Modified Mathlib/CategoryTheory/Equivalence.lean

Modified Mathlib/CategoryTheory/Filtered/Basic.lean

Modified Mathlib/CategoryTheory/Functor/ReflectsIso/Basic.lean

Modified Mathlib/CategoryTheory/GradedObject/Bifunctor.lean

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Equalizers.lean

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

Modified Mathlib/CategoryTheory/Sums/Products.lean

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

Modified Mathlib/Data/Nat/Bits.lean

Modified Mathlib/Data/Nat/Factorization/Defs.lean

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/Data/PNat/Basic.lean

Modified Mathlib/Data/PNat/Defs.lean

Modified Mathlib/Data/PNat/Factors.lean

Modified Mathlib/Data/PNat/Xgcd.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Data/WSeq/Productive.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/Dynamics/FixedPoints/Prufer.lean

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

Modified Mathlib/FieldTheory/Normal/Defs.lean

Modified Mathlib/FieldTheory/RatFunc/Defs.lean

Modified Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

Modified Mathlib/GroupTheory/Coset/Basic.lean

Modified Mathlib/GroupTheory/Coset/Card.lean

Modified Mathlib/GroupTheory/Coset/Defs.lean

Modified Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean

Modified Mathlib/GroupTheory/Sylow.lean