Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-12-22 13:19
3cfe59e7
View on Github →
chore(Algebra): fix whitespace (
#33182
) Found by extending the commandStart linter to proof bodies.
Estimated changes
Modified
Mathlib/Algebra/Category/ModuleCat/Semi.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean
Modified
Mathlib/Algebra/Category/MonCat/Colimits.lean
modified
inductive
MonCat.Colimits.Relation
Modified
Mathlib/Algebra/GradedMonoid.lean
Modified
Mathlib/Algebra/Homology/Embedding/Extend.lean
Modified
Mathlib/Algebra/Homology/HomologicalComplex.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/KInjective.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean
Modified
Mathlib/Algebra/Homology/LeftResolution/Basic.lean
Modified
Mathlib/Algebra/Homology/LocalCohomology.lean
Modified
Mathlib/Algebra/Lie/CartanExists.lean
Modified
Mathlib/Algebra/Lie/Classical.lean
Modified
Mathlib/Algebra/Lie/EngelSubalgebra.lean
Modified
Mathlib/Algebra/Lie/LieTheorem.lean
Modified
Mathlib/Algebra/Lie/TraceForm.lean
Modified
Mathlib/Algebra/Lie/Weights/RootSystem.lean
Modified
Mathlib/Algebra/Module/GradedModule.lean
Modified
Mathlib/Algebra/Module/Submodule/Pointwise.lean
Modified
Mathlib/Algebra/Module/Torsion/Basic.lean
Modified
Mathlib/Algebra/Order/Antidiag/Nat.lean
Modified
Mathlib/Algebra/Order/Archimedean/Class.lean
Modified
Mathlib/Algebra/Polynomial/Degree/Domain.lean
modified
theorem
Polynomial.natDegree_mul
Modified
Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
Modified
Mathlib/Algebra/Polynomial/HasseDeriv.lean
Modified
Mathlib/Algebra/Polynomial/Inductions.lean
Modified
Mathlib/Algebra/Polynomial/Roots.lean
Modified
Mathlib/Algebra/Polynomial/RuleOfSigns.lean
Modified
Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
Modified
Mathlib/Algebra/Ring/NegOnePow.lean
Modified
Mathlib/Algebra/Star/StarAlgHom.lean
modified
theorem
StarAlgEquiv.toAlgEquiv_injective