Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-05-15 03:04
b5606ea6
View on Github →
chore: fix more odd indents (
#24908
) Continuation of
#24893
and
#24907
, hopefully the last one.
Estimated changes
Modified
Mathlib/Analysis/Calculus/Deriv/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/Grothendieck.lean
Modified
Mathlib/GroupTheory/GroupAction/Blocks.lean
Modified
Mathlib/GroupTheory/GroupAction/Hom.lean
Modified
Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
Modified
Mathlib/GroupTheory/QuotientGroup/Defs.lean
Modified
Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
Modified
Mathlib/LinearAlgebra/BilinearForm/Basic.lean
Modified
Mathlib/LinearAlgebra/BilinearForm/Hom.lean
Modified
Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
Modified
Mathlib/LinearAlgebra/BilinearForm/Properties.lean
Modified
Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
Modified
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
Modified
Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
Modified
Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
Modified
Mathlib/LinearAlgebra/Matrix/Permutation.lean
Modified
Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
Modified
Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Reduced.lean
Modified
Mathlib/LinearAlgebra/Trace.lean
Modified
Mathlib/Logic/Equiv/Fintype.lean
Modified
Mathlib/MeasureTheory/Constructions/Pi.lean
modified
theorem
MeasureTheory.volume_preserving_arrowCongr'
Modified
Mathlib/MeasureTheory/Function/Holder.lean
Modified
Mathlib/MeasureTheory/Function/L2Space.lean
Modified
Mathlib/MeasureTheory/Group/Measure.lean
Modified
Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
Modified
Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean
Modified
Mathlib/ModelTheory/Order.lean
Modified
Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
Modified
Mathlib/NumberTheory/NumberField/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/Completion.lean
Modified
Mathlib/NumberTheory/NumberField/House.lean
Modified
Mathlib/NumberTheory/Padics/ProperSpace.lean
Modified
Mathlib/NumberTheory/PythagoreanTriples.lean
Modified
Mathlib/NumberTheory/SelbergSieve.lean
Modified
Mathlib/Order/CompactlyGenerated/Basic.lean
Modified
Mathlib/Order/Filter/Pointwise.lean
Modified
Mathlib/Order/Heyting/Basic.lean
Modified
Mathlib/Order/WellFoundedSet.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/Maps.lean
Modified
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
Modified
Mathlib/RingTheory/DedekindDomain/Ideal.lean
Modified
Mathlib/RingTheory/Flat/Basic.lean
Modified
Mathlib/RingTheory/Ideal/Height.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/Basic.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/Defs.lean
Modified
Mathlib/RingTheory/Jacobson/Ring.lean
Modified
Mathlib/RingTheory/LaurentSeries.lean
Modified
Mathlib/RingTheory/LocalProperties/Basic.lean
Modified
Mathlib/RingTheory/MvPolynomial/Groebner.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Basic.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Inverse.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Order.lean
Modified
Mathlib/RingTheory/Polynomial/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Content.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
Modified
Mathlib/RingTheory/PowerSeries/Basic.lean
Modified
Mathlib/RingTheory/PowerSeries/NoZeroDivisors.lean
Modified
Mathlib/RingTheory/Unramified/Basic.lean
Modified
Mathlib/SetTheory/Ordinal/Veblen.lean
Modified
Mathlib/SetTheory/PGame/Order.lean
Modified
Mathlib/Tactic/FunProp.lean
Modified
Mathlib/Tactic/Linter/Multigoal.lean
Modified
Mathlib/Tactic/NoncommRing.lean
Modified
Mathlib/Tactic/NormNum/Core.lean
Modified
Mathlib/Topology/Algebra/Nonarchimedean/TotallyDisconnected.lean
Modified
Mathlib/Topology/Algebra/Order/Archimedean.lean
Modified
Mathlib/Topology/Algebra/TopologicallyNilpotent.lean
modified
theorem
IsTopologicallyNilpotent.mul_left
modified
theorem
IsTopologicallyNilpotent.mul_left_of_commute
Modified
Mathlib/Topology/Algebra/Valued/WithVal.lean
Modified
Mathlib/Topology/Clopen.lean
Modified
Mathlib/Topology/Compactification/OnePointEquiv.lean
Modified
Mathlib/Topology/Compactness/LocallyCompact.lean
Modified
Mathlib/Topology/Defs/Sequences.lean
Modified
Mathlib/Topology/Instances/NNReal/Lemmas.lean
Modified
Mathlib/Topology/MetricSpace/CauSeqFilter.lean
Modified
Mathlib/Topology/MetricSpace/Holder.lean
Modified
Mathlib/Topology/Order/LeftRightNhds.lean
Modified
Mathlib/Topology/Order/MonotoneConvergence.lean
Modified
Mathlib/Topology/UniformSpace/AbstractCompletion.lean
Modified
Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean
Modified
Mathlib/Topology/UniformSpace/UniformApproximation.lean
Modified
Mathlib/Topology/UniformSpace/UniformConvergence.lean
Modified
MathlibTest/Simps.lean
Modified
MathlibTest/linarith.lean
Modified
Shake/Main.lean