Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-04-01 16:53
08686b25
View on Github →
chore: avoid Ne.def (adaptation for nightly-2024-03-27) (
#11813
)
Estimated changes
Modified
Mathlib/MeasureTheory/Covering/LiminfLimsup.lean
Modified
Mathlib/MeasureTheory/Covering/Vitali.lean
Modified
Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
Modified
Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
Modified
Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
Modified
Mathlib/MeasureTheory/Function/Jacobian.lean
Modified
Mathlib/MeasureTheory/Function/L1Space.lean
Modified
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
Modified
Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
Modified
Mathlib/MeasureTheory/Function/SimpleFunc.lean
Modified
Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
Modified
Mathlib/MeasureTheory/Function/UniformIntegrable.lean
Modified
Mathlib/MeasureTheory/Group/AddCircle.lean
Modified
Mathlib/MeasureTheory/Group/FundamentalDomain.lean
Modified
Mathlib/MeasureTheory/Integral/Average.lean
Modified
Mathlib/MeasureTheory/Integral/Bochner.lean
Modified
Mathlib/MeasureTheory/Integral/CircleIntegral.lean
Modified
Mathlib/MeasureTheory/Integral/IntegrableOn.lean
Modified
Mathlib/MeasureTheory/Integral/Lebesgue.lean
Modified
Mathlib/MeasureTheory/Integral/LebesgueNormedSpace.lean
Modified
Mathlib/MeasureTheory/Integral/SetIntegral.lean
Modified
Mathlib/MeasureTheory/Integral/SetToL1.lean
Modified
Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean
Modified
Mathlib/MeasureTheory/Measure/AddContent.lean
Modified
Mathlib/MeasureTheory/Measure/Count.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
Modified
Mathlib/MeasureTheory/Measure/Hausdorff.lean
Modified
Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
Modified
Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
Modified
Mathlib/MeasureTheory/Measure/MeasureSpace.lean
Modified
Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/Regular.lean
Modified
Mathlib/MeasureTheory/Measure/WithDensity.lean
Modified
Mathlib/ModelTheory/Semantics.lean
Modified
Mathlib/ModelTheory/Types.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction.lean
Modified
Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean
Modified
Mathlib/NumberTheory/ClassNumber/Finite.lean
Modified
Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
Modified
Mathlib/NumberTheory/Divisors.lean
Modified
Mathlib/NumberTheory/FunctionField.lean
Modified
Mathlib/NumberTheory/KummerDedekind.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean
Modified
Mathlib/NumberTheory/Liouville/Basic.lean
Modified
Mathlib/NumberTheory/Liouville/LiouvilleWith.lean
Modified
Mathlib/NumberTheory/LucasLehmer.lean
Modified
Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
Modified
Mathlib/NumberTheory/NumberField/Embeddings.lean
Modified
Mathlib/NumberTheory/Padics/PadicNumbers.lean
Modified
Mathlib/NumberTheory/Padics/PadicVal.lean
Modified
Mathlib/NumberTheory/PythagoreanTriples.lean
Modified
Mathlib/NumberTheory/RamificationInertia.lean
Modified
Mathlib/NumberTheory/SumTwoSquares.lean
Modified
Mathlib/NumberTheory/VonMangoldt.lean
Modified
Mathlib/NumberTheory/ZetaFunction.lean
Modified
Mathlib/NumberTheory/ZetaValues.lean
Modified
Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
Modified
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
Modified
Mathlib/Order/Filter/Basic.lean
Modified
Mathlib/Order/Filter/Lift.lean
Modified
Mathlib/Order/Filter/Ultrafilter.lean
Modified
Mathlib/Order/JordanHolder.lean
Modified
Mathlib/Order/Lattice.lean
modified
theorem
inf_lt_sup
Modified
Mathlib/Order/Partition/Finpartition.lean
Modified
Mathlib/Order/SupIndep.lean
Modified
Mathlib/Probability/Distributions/Uniform.lean
Modified
Mathlib/Probability/Martingale/Convergence.lean
Modified
Mathlib/Probability/Moments.lean
Modified
Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
Modified
Mathlib/Probability/ProbabilityMassFunction/Monad.lean
Modified
Mathlib/Probability/Variance.lean
Modified
Mathlib/RingTheory/AdjoinRoot.lean
Modified
Mathlib/RingTheory/Algebraic.lean
Modified
Mathlib/RingTheory/ChainOfDivisors.lean
Modified
Mathlib/RingTheory/Coprime/Lemmas.lean
Modified
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
Modified
Mathlib/RingTheory/DedekindDomain/Factorization.lean
Modified
Mathlib/RingTheory/DedekindDomain/Ideal.lean
Modified
Mathlib/RingTheory/DedekindDomain/PID.lean
Modified
Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
Modified
Mathlib/RingTheory/EisensteinCriterion.lean
Modified
Mathlib/RingTheory/FractionalIdeal/Operations.lean
Modified
Mathlib/RingTheory/GradedAlgebra/Radical.lean
Modified
Mathlib/RingTheory/HahnSeries/Basic.lean
Modified
Mathlib/RingTheory/HahnSeries/Multiplication.lean
Modified
Mathlib/RingTheory/Ideal/AssociatedPrime.lean
Modified
Mathlib/RingTheory/Ideal/Basic.lean
Modified
Mathlib/RingTheory/Ideal/Norm.lean
Modified
Mathlib/RingTheory/Ideal/Operations.lean
Modified
Mathlib/RingTheory/Ideal/Over.lean
Modified
Mathlib/RingTheory/Int/Basic.lean
Modified
Mathlib/RingTheory/IntegralClosure.lean
Modified
Mathlib/RingTheory/IsAdjoinRoot.lean
Modified
Mathlib/RingTheory/Jacobson.lean
Modified
Mathlib/RingTheory/LaurentSeries.lean
Modified
Mathlib/RingTheory/Localization/FractionRing.lean
Modified
Mathlib/RingTheory/Localization/Integral.lean
Modified
Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
Modified
Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Bernstein.lean
Modified
Mathlib/RingTheory/Polynomial/Content.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
Modified
Mathlib/RingTheory/Polynomial/Dickson.lean
Modified
Mathlib/RingTheory/Polynomial/GaussLemma.lean
Modified
Mathlib/RingTheory/Polynomial/Opposites.lean
Modified
Mathlib/RingTheory/PolynomialAlgebra.lean
Modified
Mathlib/RingTheory/PowerSeries/Basic.lean
Modified
Mathlib/RingTheory/RootsOfUnity/Basic.lean
Modified
Mathlib/RingTheory/RootsOfUnity/Complex.lean
Modified
Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
Modified
Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
Modified
Mathlib/RingTheory/WittVector/MulCoeff.lean
Modified
Mathlib/SetTheory/Cardinal/ENat.lean
Modified
Mathlib/Testing/SlimCheck/Functions.lean
Modified
Mathlib/Topology/Algebra/ConstMulAction.lean
Modified
Mathlib/Topology/Algebra/Group/Basic.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Group.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
Modified
Mathlib/Topology/Basic.lean
Modified
Mathlib/Topology/Connected/Basic.lean
Modified
Mathlib/Topology/EMetricSpace/Basic.lean
Modified
Mathlib/Topology/Instances/ENNReal.lean
Modified
Mathlib/Topology/MetricSpace/CantorScheme.lean
Modified
Mathlib/Topology/MetricSpace/Gluing.lean
Modified
Mathlib/Topology/MetricSpace/HausdorffDistance.lean
Modified
Mathlib/Topology/MetricSpace/Infsep.lean
Modified
Mathlib/Topology/MetricSpace/PiNat.lean
Modified
Mathlib/Topology/PartitionOfUnity.lean
Modified
Mathlib/Topology/Separation.lean
Modified
Mathlib/Topology/Sets/Opens.lean