Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-07-26 23:35
d421f15d
View on Github →
chore: more indentation fixes (
#27502
) Found by the linter in
#27473
.
Estimated changes
Modified
Mathlib/Algebra/Algebra/NonUnitalHom.lean
Modified
Mathlib/Algebra/Azumaya/Defs.lean
Modified
Mathlib/Algebra/Category/FGModuleCat/Basic.lean
Modified
Mathlib/Algebra/Category/Grp/Basic.lean
modified
theorem
CommGrp.hom_ofHom
Modified
Mathlib/Algebra/Category/Grp/Limits.lean
Modified
Mathlib/Algebra/Category/GrpWithZero.lean
modified
theorem
GrpWithZero.forget_map
Modified
Mathlib/Algebra/Category/ModuleCat/Colimits.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean
modified
theorem
TopModuleCat.hom_id
modified
theorem
TopModuleCat.hom_smul
modified
theorem
TopModuleCat.ofHom_hom
Modified
Mathlib/Algebra/Category/MonCat/FilteredColimits.lean
Modified
Mathlib/Algebra/Category/Ring/Basic.lean
modified
theorem
CommRingCat.hom_ofHom
Modified
Mathlib/Algebra/Category/Ring/Constructions.lean
modified
theorem
CommRingCat.coproductCocone_inl
modified
theorem
CommRingCat.coproductCocone_inr
Modified
Mathlib/Algebra/Group/Subgroup/Map.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean
modified
theorem
CategoryTheory.hasExt_of_enoughProjectives
Modified
Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Homology.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
Modified
Mathlib/Algebra/Module/Submodule/Pointwise.lean
Modified
Mathlib/Algebra/Module/Submodule/Range.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Defs.lean
modified
theorem
AddMonoidAlgebra.singleAddHom_apply
modified
theorem
MonoidAlgebra.singleAddHom_apply
Modified
Mathlib/Algebra/Polynomial/Basic.lean
Modified
Mathlib/Algebra/Polynomial/Coeff.lean
Modified
Mathlib/Algebra/Polynomial/Laurent.lean
modified
theorem
LaurentPolynomial.eval₂_C_mul_T_neg_n
Modified
Mathlib/Algebra/RingQuot.lean
Modified
Mathlib/Analysis/InnerProductSpace/Basic.lean
Modified
Mathlib/CategoryTheory/Adjunction/Reflective.lean
Modified
Mathlib/CategoryTheory/GradedObject.lean
Modified
Mathlib/CategoryTheory/GradedObject/Bifunctor.lean
Modified
Mathlib/CategoryTheory/GradedObject/Trifunctor.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
Modified
Mathlib/CategoryTheory/Linear/LinearFunctor.lean
Modified
Mathlib/CategoryTheory/Monoidal/Comon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/End.lean
Modified
Mathlib/CategoryTheory/Monoidal/Functor.lean
Modified
Mathlib/CategoryTheory/Monoidal/Mon_.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Comma.lean
modified
theorem
CategoryTheory.MorphismProperty.Comma.Hom.hom_mk
Modified
Mathlib/CategoryTheory/Preadditive/LeftExact.lean
Modified
Mathlib/CategoryTheory/Shift/Basic.lean
Modified
Mathlib/CategoryTheory/Subterminal.lean
Modified
Mathlib/CategoryTheory/WithTerminal/Cone.lean
Modified
Mathlib/Data/Finsupp/SMulWithZero.lean
Modified
Mathlib/Data/Fintype/Powerset.lean
Modified
Mathlib/Data/Matrix/Basic.lean
Modified
Mathlib/Data/Matrix/Composition.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/GroupTheory/OrderOfElement.lean
Modified
Mathlib/LinearAlgebra/BilinearMap.lean
Modified
Mathlib/LinearAlgebra/Multilinear/Basic.lean
Modified
Mathlib/Order/Category/BddDistLat.lean
Modified
Mathlib/Order/Category/BddOrd.lean
Modified
Mathlib/Order/Category/BoolAlg.lean
Modified
Mathlib/Order/Category/DistLat.lean
Modified
Mathlib/Order/Category/FinPartOrd.lean
Modified
Mathlib/Order/Category/HeytAlg.lean
Modified
Mathlib/Order/Category/Lat.lean
modified
theorem
Lat.hom_ofHom
Modified
Mathlib/Order/Category/PartOrd.lean
Modified
Mathlib/Order/RelSeries.lean
Modified
Mathlib/RingTheory/HahnSeries/Multiplication.lean
Modified
Mathlib/RingTheory/Ideal/Operations.lean
Modified
Mathlib/RingTheory/Localization/Basic.lean
Modified
Mathlib/SetTheory/Cardinal/ENat.lean
Modified
Mathlib/Topology/Category/TopCat/Basic.lean
Modified
Mathlib/Topology/Constructions/SumProd.lean
Modified
Mathlib/Topology/DiscreteSubset.lean
Modified
Mathlib/Topology/Homeomorph/Defs.lean