Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-04-30 06:07
45f93f3f
View on Github →
chore: adapt to multiple goal linter 1 (
#12338
) A PR accompanying
#12339
.
Zulip discussion
Estimated changes
Modified
Archive/Imo/Imo1972Q5.lean
Modified
Archive/Imo/Imo2008Q2.lean
Modified
Archive/Wiedijk100Theorems/AbelRuffini.lean
Modified
Archive/Wiedijk100Theorems/BallotProblem.lean
Modified
Archive/Wiedijk100Theorems/CubingACube.lean
Modified
Archive/Wiedijk100Theorems/Partition.lean
Modified
Counterexamples/Cyclotomic105.lean
Modified
Counterexamples/DirectSumIsInternal.lean
Modified
Mathlib/Algebra/BigOperators/Finprod.lean
Modified
Mathlib/Algebra/BigOperators/List/Basic.lean
Modified
Mathlib/Algebra/Category/Ring/Constructions.lean
Modified
Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
Modified
Mathlib/Algebra/GCDMonoid/Finset.lean
Modified
Mathlib/Algebra/GeomSum.lean
Modified
Mathlib/Algebra/GroupPower/Order.lean
Modified
Mathlib/Algebra/Lie/DirectSum.lean
Modified
Mathlib/Algebra/Lie/IdealOperations.lean
Modified
Mathlib/Algebra/Module/LinearMap/End.lean
Modified
Mathlib/Algebra/Order/BigOperators/Group/List.lean
Modified
Mathlib/Algebra/Order/CauSeq/BigOperators.lean
Modified
Mathlib/Algebra/Order/Field/Basic.lean
Modified
Mathlib/Algebra/Order/Group/Int.lean
Modified
Mathlib/Algebra/Order/Group/MinMax.lean
Modified
Mathlib/Algebra/Order/Interval/Basic.lean
Modified
Mathlib/Algebra/Order/Pointwise.lean
Modified
Mathlib/Algebra/Order/Sub/Defs.lean
Modified
Mathlib/Algebra/Quandle.lean
Modified
Mathlib/AlgebraicGeometry/Gluing.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
Modified
Mathlib/Analysis/Calculus/ParametricIntegral.lean
Modified
Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
Modified
Mathlib/Analysis/Complex/Polynomial.lean
Modified
Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
Modified
Mathlib/CategoryTheory/Category/Quiv.lean
Modified
Mathlib/CategoryTheory/GlueData.lean
Modified
Mathlib/CategoryTheory/IsConnected.lean
Modified
Mathlib/CategoryTheory/Limits/Connected.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean
Modified
Mathlib/CategoryTheory/Limits/Final.lean
Modified
Mathlib/CategoryTheory/Limits/Fubini.lean
Modified
Mathlib/CategoryTheory/Limits/KanExtension.lean
Modified
Mathlib/CategoryTheory/Limits/Lattice.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Presheaf.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
Modified
Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/Canonical.lean
Modified
Mathlib/CategoryTheory/Sites/Coverage.lean
Modified
Mathlib/CategoryTheory/Subobject/MonoOver.lean
Modified
Mathlib/Combinatorics/Enumerative/Composition.lean
Modified
Mathlib/Combinatorics/Quiver/Arborescence.lean
Modified
Mathlib/Combinatorics/SetFamily/FourFunctions.lean
Modified
Mathlib/Combinatorics/SetFamily/LYM.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Density.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Maps.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Prod.lean
Modified
Mathlib/Combinatorics/Young/YoungDiagram.lean
Modified
Mathlib/Computability/RegularExpressions.lean
Modified
Mathlib/Computability/TMToPartrec.lean
Modified
Mathlib/Computability/TuringMachine.lean
Modified
Mathlib/Control/Fix.lean
Modified
Mathlib/Control/LawfulFix.lean
Modified
Mathlib/Data/Analysis/Filter.lean
Modified
Mathlib/Data/DFinsupp/Basic.lean
Modified
Mathlib/Data/Fin/Basic.lean
Modified
Mathlib/Data/FinEnum.lean
Modified
Mathlib/Data/Finset/Lattice.lean
Modified
Mathlib/Data/Finset/NoncommProd.lean
Modified
Mathlib/Data/Finset/Sym.lean
Modified
Mathlib/Data/Finsupp/Basic.lean
Modified
Mathlib/Data/Finsupp/Defs.lean
Modified
Mathlib/Data/Fintype/Quotient.lean
Modified
Mathlib/Data/Int/Bitwise.lean
Modified
Mathlib/Data/List/Basic.lean
Modified
Mathlib/Data/List/Chain.lean
Modified
Mathlib/Data/List/Cycle.lean
Modified
Mathlib/Data/List/Dedup.lean
Modified
Mathlib/Data/List/Indexes.lean
Modified
Mathlib/Data/List/MinMax.lean
Modified
Mathlib/Data/List/Perm.lean
Modified
Mathlib/Data/List/Permutation.lean
Modified
Mathlib/Data/List/Sigma.lean
Modified
Mathlib/Data/List/Sublists.lean
Modified
Mathlib/Data/List/Zip.lean
Modified
Mathlib/Data/Multiset/Antidiagonal.lean
Modified
Mathlib/Data/Multiset/Pi.lean
Modified
Mathlib/Data/Multiset/Sum.lean
Modified
Mathlib/Data/NNRat/Defs.lean
Modified
Mathlib/Data/Nat/Bits.lean
Modified
Mathlib/Data/Nat/Cast/Field.lean
Modified
Mathlib/Data/Nat/Defs.lean
Modified
Mathlib/Data/Nat/EvenOddRec.lean
Modified
Mathlib/Data/Nat/Fib/Zeckendorf.lean
Modified
Mathlib/Data/Nat/Lattice.lean
Modified
Mathlib/Data/Nat/ModEq.lean
Modified
Mathlib/Data/Nat/PSub.lean
Modified
Mathlib/Data/Nat/Pairing.lean
Modified
Mathlib/Data/Nat/WithBot.lean
Modified
Mathlib/Data/Num/Lemmas.lean
Modified
Mathlib/Data/Ordmap/Ordset.lean
Modified
Mathlib/Data/PFunctor/Multivariate/M.lean
Modified
Mathlib/Data/PFunctor/Univariate/M.lean
Modified
Mathlib/Data/PNat/Factors.lean
Modified
Mathlib/Data/PNat/Prime.lean
Modified
Mathlib/Data/PNat/Xgcd.lean
Modified
Mathlib/Data/Pi/Lex.lean
Modified
Mathlib/Data/Prod/TProd.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
Modified
Mathlib/Data/QPF/Univariate/Basic.lean
Modified
Mathlib/Data/Rat/Cast/Defs.lean
Modified
Mathlib/Data/Rat/Defs.lean
Modified
Mathlib/Data/Rat/Lemmas.lean
Modified
Mathlib/Data/Seq/Parallel.lean
Modified
Mathlib/Data/Seq/Seq.lean
Modified
Mathlib/Data/Seq/WSeq.lean
Modified
Mathlib/Data/Set/Image.lean
Modified
Mathlib/Data/Stream/Init.lean
Modified
Mathlib/Data/Sum/Interval.lean
Modified
Mathlib/Data/Sum/Order.lean
Modified
Mathlib/Data/TypeVec.lean
Modified
Mathlib/Data/UInt.lean
Modified
Mathlib/Data/Vector/Basic.lean
Modified
Mathlib/Data/Vector3.lean
Modified
Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
Modified
Mathlib/GroupTheory/Congruence.lean
Modified
Mathlib/GroupTheory/CoprodI.lean
Modified
Mathlib/GroupTheory/MonoidLocalization.lean
Modified
Mathlib/GroupTheory/Perm/ClosureSwap.lean
Modified
Mathlib/GroupTheory/Perm/Option.lean
Modified
Mathlib/GroupTheory/Perm/Support.lean
Modified
Mathlib/GroupTheory/Subgroup/Basic.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
Modified
Mathlib/LinearAlgebra/FiniteDimensional.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent.lean
Modified
Mathlib/LinearAlgebra/Matrix/Block.lean
Modified
Mathlib/Logic/Relation.lean
Modified
Mathlib/MeasureTheory/Decomposition/Jordan.lean
Modified
Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
Modified
Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
Modified
Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
Modified
Mathlib/MeasureTheory/Group/Convolution.lean
Modified
Mathlib/MeasureTheory/Group/FundamentalDomain.lean
Modified
Mathlib/MeasureTheory/Integral/Average.lean
Modified
Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
Modified
Mathlib/MeasureTheory/Integral/Lebesgue.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
Modified
Mathlib/MeasureTheory/Measure/Content.lean
Modified
Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
Modified
Mathlib/MeasureTheory/Measure/Sub.lean
Modified
Mathlib/MeasureTheory/Measure/VectorMeasure.lean
Modified
Mathlib/NumberTheory/ADEInequality.lean
Modified
Mathlib/NumberTheory/Cyclotomic/Rat.lean
Modified
Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
Modified
Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
Modified
Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
Modified
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
Modified
Mathlib/NumberTheory/NumberField/Units.lean
Modified
Mathlib/Order/CompactlyGenerated/Basic.lean
Modified
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
Modified
Mathlib/Order/Extension/Linear.lean
Modified
Mathlib/Order/Filter/AtTopBot.lean
Modified
Mathlib/Order/Filter/Basic.lean
Modified
Mathlib/Order/Filter/Prod.lean
Modified
Mathlib/Order/Interval/Basic.lean
Modified
Mathlib/Order/Iterate.lean
Modified
Mathlib/Order/Minimal.lean
Modified
Mathlib/Order/OmegaCompletePartialOrder.lean
Modified
Mathlib/Order/RelSeries.lean
Modified
Mathlib/Order/WellFounded.lean
Modified
Mathlib/Order/WellFoundedSet.lean
Modified
Mathlib/Probability/Kernel/MeasurableIntegral.lean
Modified
Mathlib/Probability/StrongLaw.lean
Modified
Mathlib/RingTheory/HahnSeries/Basic.lean
Modified
Mathlib/RingTheory/Ideal/Cotangent.lean
Modified
Mathlib/RingTheory/Multiplicity.lean
Modified
Mathlib/SetTheory/Game/Basic.lean
Modified
Mathlib/SetTheory/Ordinal/Arithmetic.lean
Modified
Mathlib/Tactic/CancelDenoms/Core.lean
Modified
Mathlib/Testing/SlimCheck/Gen.lean
Modified
Mathlib/Topology/Basic.lean
Modified
Mathlib/Topology/ContinuousFunction/Bounded.lean
Modified
Mathlib/Topology/TietzeExtension.lean