Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-07-25 22:49
8271ba97
View on Github →
chore: fix more indentation (
#27494
) Found by the linter in
#27473
.
Estimated changes
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
Modified
Mathlib/Algebra/Group/AddChar.lean
Modified
Mathlib/Algebra/Group/ConjFinite.lean
Modified
Mathlib/Algebra/Homology/BifunctorAssociator.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughInjectives.lean
modified
theorem
CategoryTheory.hasExt_of_enoughInjectives
Modified
Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean
Modified
Mathlib/Algebra/Homology/HomologicalComplexLimits.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
Modified
Mathlib/Algebra/Homology/Linear.lean
Modified
Mathlib/Algebra/Lie/Submodule.lean
Modified
Mathlib/Algebra/Order/Antidiag/Nat.lean
Modified
Mathlib/Algebra/Star/CHSH.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean
Modified
Mathlib/AlgebraicGeometry/Limits.lean
Modified
Mathlib/AlgebraicGeometry/Modules/Tilde.lean
modified
theorem
ModuleCat.Tilde.sections_smul_localizations_def
Modified
Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
Modified
Mathlib/AlgebraicGeometry/Restrict.lean
Modified
Mathlib/AlgebraicGeometry/Sites/Representability.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/Cylinder.lean
modified
theorem
HomotopicalAlgebra.Precylinder.symm_i
Modified
Mathlib/AlgebraicTopology/Quasicategory/Nerve.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
Modified
Mathlib/Analysis/Analytic/Order.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
Modified
Mathlib/Analysis/Calculus/LHopital.lean
Modified
Mathlib/Analysis/Convex/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/Defs.lean
Modified
Mathlib/Analysis/Normed/Group/Quotient.lean
Modified
Mathlib/Analysis/Normed/Group/SemiNormedGrp/Completion.lean
Modified
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
Modified
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
Modified
Mathlib/Analysis/Oscillation.lean
Modified
Mathlib/CategoryTheory/Bicategory/CatEnriched.lean
Modified
Mathlib/CategoryTheory/Category/Quiv.lean
Modified
Mathlib/CategoryTheory/Category/ReflQuiv.lean
Modified
Mathlib/CategoryTheory/Distributive/Monoidal.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean
Modified
Mathlib/CategoryTheory/GradedObject/Monoidal.lean
Modified
Mathlib/CategoryTheory/GradedObject/Trifunctor.lean
Modified
Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean
Modified
Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
modified
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mk
Modified
Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean
Modified
Mathlib/CategoryTheory/Localization/Triangulated.lean
Modified
Mathlib/CategoryTheory/Monad/Comonadicity.lean
Modified
Mathlib/CategoryTheory/Monad/Monadicity.lean
Modified
Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution.lean
Modified
Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean
Modified
Mathlib/CategoryTheory/Shift/CommShift.lean
Modified
Mathlib/CategoryTheory/Sites/CompatiblePlus.lean
Modified
Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
Modified
Mathlib/CategoryTheory/Topos/Classifier.lean
modified
theorem
CategoryTheory.HasClassifier.unique
Modified
Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
Modified
Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Copy.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Maps.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
Modified
Mathlib/Computability/TuringMachine.lean
Modified
Mathlib/Data/Matrix/Bilinear.lean
modified
theorem
mulLeftLinearMap_zero_eq_zero
modified
theorem
mulRightLinearMap_zero_eq_zero
Modified
Mathlib/FieldTheory/AlgebraicClosure.lean
modified
theorem
algebraicClosure_toSubalgebra
Modified
Mathlib/FieldTheory/JacobsonNoether.lean
Modified
Mathlib/FieldTheory/NormalizedTrace.lean
Modified
Mathlib/Geometry/Euclidean/MongePoint.lean
Modified
Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
Modified
Mathlib/GroupTheory/ClassEquation.lean
Modified
Mathlib/GroupTheory/Coxeter/Basic.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
Modified
Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
Modified
Mathlib/LinearAlgebra/FreeModule/PID.lean
Modified
Mathlib/LinearAlgebra/FreeProduct/Basic.lean
Modified
Mathlib/LinearAlgebra/Lagrange.lean
Modified
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
Modified
Mathlib/MeasureTheory/Measure/Content.lean
Modified
Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
Modified
Mathlib/NumberTheory/LSeries/SumCoeff.lean
Modified
Mathlib/NumberTheory/NumberField/AdeleRing.lean
Modified
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
modified
theorem
NumberField.mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior
Modified
Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean
Modified
Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
modified
theorem
NumberField.InfinitePlace.coe_apply
Modified
Mathlib/NumberTheory/NumberField/Norm.lean
modified
theorem
RingOfIntegers.coe_norm
Modified
Mathlib/Order/Category/FinBddDistLat.lean
Modified
Mathlib/Order/Category/Frm.lean
modified
theorem
Frm.hom_ofHom
Modified
Mathlib/Order/Category/LinOrd.lean
modified
theorem
LinOrd.hom_ofHom
Modified
Mathlib/Order/Category/NonemptyFinLinOrd.lean
Modified
Mathlib/Order/CompleteSublattice.lean
Modified
Mathlib/RepresentationTheory/Coinvariants.lean
Modified
Mathlib/RingTheory/ClassGroup.lean
Modified
Mathlib/RingTheory/DedekindDomain/Different.lean
Modified
Mathlib/RingTheory/DividedPowers/DPMorphism.lean
Modified
Mathlib/RingTheory/HahnSeries/Multiplication.lean
Modified
Mathlib/RingTheory/Jacobson/Ring.lean
Modified
Mathlib/RingTheory/Kaehler/TensorProduct.lean
Modified
Mathlib/RingTheory/LittleWedderburn.lean
Modified
Mathlib/RingTheory/NoetherNormalization.lean
Modified
Mathlib/RingTheory/PowerSeries/Substitution.lean
modified
theorem
PowerSeries.HasSubst.comp
modified
theorem
PowerSeries.HasSubst.smul
modified
theorem
PowerSeries.substAlgHom_comp_substAlgHom
modified
theorem
PowerSeries.substAlgHom_comp_substAlgHom_apply
modified
theorem
PowerSeries.subst_comp_subst_apply
Modified
Mathlib/RingTheory/Smooth/StandardSmooth.lean
Modified
Mathlib/RingTheory/Valuation/Basic.lean
modified
theorem
Valuation.ofAddValuation_toAddValuation
Modified
Mathlib/RingTheory/Valuation/Extension.lean
Modified
Mathlib/RingTheory/Valuation/ValuationSubring.lean
Modified
Mathlib/SetTheory/Descriptive/Tree.lean
modified
theorem
Descriptive.Tree.mem_pullSub_long
modified
theorem
Descriptive.Tree.mem_pullSub_short
modified
theorem
Descriptive.Tree.take_take
Modified
Mathlib/SetTheory/Ordinal/Veblen.lean
Modified
Mathlib/SetTheory/ZFC/Class.lean
Modified
Mathlib/Tactic/Positivity/Finset.lean
Modified
Mathlib/Topology/Algebra/Algebra.lean
modified
theorem
Subalgebra.topologicalClosure_coe
Modified
Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean
Modified
Mathlib/Topology/CWComplex/Classical/Basic.lean
Modified
Mathlib/Topology/Category/LightProfinite/Extend.lean
Modified
Mathlib/Topology/Category/TopCat/ULift.lean
Modified
Mathlib/Topology/EMetricSpace/Defs.lean
Modified
Mathlib/Topology/Order/Category/AlexDisc.lean
Modified
Mathlib/Topology/Sheaves/Stalks.lean
Modified
Mathlib/Topology/Specialization.lean