Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-03-30 20:20
1b40c7bc
View on Github →
chore: avoid Ne.def (adaptation for nightly-2024-03-27) (
#11801
)
Estimated changes
Modified
Archive/Imo/Imo2005Q4.lean
Modified
Archive/Wiedijk100Theorems/BallotProblem.lean
Modified
Archive/Wiedijk100Theorems/CubingACube.lean
Modified
Archive/Wiedijk100Theorems/FriendshipGraphs.lean
Modified
Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean
Modified
Mathlib/Algebra/BigOperators/Basic.lean
Modified
Mathlib/Algebra/BigOperators/Finprod.lean
Modified
Mathlib/Algebra/CharP/Basic.lean
Modified
Mathlib/Algebra/CharP/MixedCharZero.lean
Modified
Mathlib/Algebra/Function/Support.lean
Modified
Mathlib/Algebra/GeomSum.lean
Modified
Mathlib/Algebra/GroupWithZero/Power.lean
Modified
Mathlib/Algebra/Lie/Engel.lean
Modified
Mathlib/Algebra/Lie/Weights/Linear.lean
Modified
Mathlib/Algebra/Module/Basic.lean
modified
theorem
smul_ne_zero_iff
Modified
Mathlib/Algebra/MonoidAlgebra/Support.lean
Modified
Mathlib/Algebra/Order/Module/OrderedSMul.lean
Modified
Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
Modified
Mathlib/Algebra/Order/Rearrangement.lean
Modified
Mathlib/Algebra/Order/Ring/WithTop.lean
Modified
Mathlib/Algebra/Order/Sub/Canonical.lean
Modified
Mathlib/Algebra/Order/Sub/WithTop.lean
Modified
Mathlib/Algebra/Parity.lean
Modified
Mathlib/Algebra/Polynomial/BigOperators.lean
Modified
Mathlib/AlgebraicGeometry/FunctionField.lean
Modified
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
Modified
Mathlib/AlgebraicGeometry/Properties.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
Modified
Mathlib/Analysis/Analytic/Composition.lean
Modified
Mathlib/Analysis/Analytic/Inverse.lean
Modified
Mathlib/Analysis/BoxIntegral/Partition/Split.lean
Modified
Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
Modified
Mathlib/Analysis/Calculus/BumpFunction/InnerProduct.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
Modified
Mathlib/Analysis/Calculus/LagrangeMultipliers.lean
Modified
Mathlib/Analysis/Calculus/TangentCone.lean
Modified
Mathlib/Analysis/Calculus/Taylor.lean
Modified
Mathlib/Analysis/Complex/Conformal.lean
Modified
Mathlib/Analysis/Complex/OpenMapping.lean
Modified
Mathlib/Analysis/Complex/RealDeriv.lean
Modified
Mathlib/Analysis/Complex/RemovableSingularity.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
Modified
Mathlib/Analysis/ConstantSpeed.lean
Modified
Mathlib/Analysis/Convex/Caratheodory.lean
Modified
Mathlib/Analysis/Convex/Combination.lean
Modified
Mathlib/Analysis/Convex/Gauge.lean
Modified
Mathlib/Analysis/Convex/Hull.lean
Modified
Mathlib/Analysis/Convex/StrictConvexSpace.lean
Modified
Mathlib/Analysis/InnerProductSpace/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
Modified
Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
Modified
Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean
Modified
Mathlib/Analysis/MeanInequalities.lean
Modified
Mathlib/Analysis/MeanInequalitiesPow.lean
Modified
Mathlib/Analysis/MellinTransform.lean
Modified
Mathlib/Analysis/NormedSpace/Basic.lean
Modified
Mathlib/Analysis/NormedSpace/Dual.lean
Modified
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
Modified
Mathlib/Analysis/NormedSpace/Star/Basic.lean
Modified
Mathlib/Analysis/NormedSpace/Units.lean
Modified
Mathlib/Analysis/NormedSpace/lpSpace.lean
Modified
Mathlib/Analysis/PSeries.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gaussian.lean
Modified
Mathlib/Analysis/SpecialFunctions/Integrals.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Base.lean
Modified
Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
Modified
Mathlib/Analysis/SpecificLimits/FloorPow.lean
Modified
Mathlib/CategoryTheory/Extensive.lean
Modified
Mathlib/CategoryTheory/Preadditive/Schur.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Basic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Clique.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Coloring.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
Modified
Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Partition.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Trails.lean
Modified
Mathlib/Computability/RegularExpressions.lean
Modified
Mathlib/Data/Complex/Module.lean
Modified
Mathlib/Data/DFinsupp/Basic.lean
Modified
Mathlib/Data/DFinsupp/NeLocus.lean
Modified
Mathlib/Data/DFinsupp/Order.lean
Modified
Mathlib/Data/ENNReal/Inv.lean
Modified
Mathlib/Data/ENNReal/Operations.lean
Modified
Mathlib/Data/ENat/Lattice.lean
Modified
Mathlib/Data/Fin/Basic.lean
Modified
Mathlib/Data/Fin/Tuple/Basic.lean
Modified
Mathlib/Data/Finset/Basic.lean
Modified
Mathlib/Data/Finset/Image.lean
Modified
Mathlib/Data/Finsupp/Basic.lean
Modified
Mathlib/Data/Finsupp/Defs.lean
Modified
Mathlib/Data/Finsupp/NeLocus.lean
Modified
Mathlib/Data/Finsupp/Order.lean
Modified
Mathlib/Data/Finsupp/Pointwise.lean
Modified
Mathlib/Data/Finsupp/ToDFinsupp.lean
Modified
Mathlib/Data/Fintype/Perm.lean
Modified
Mathlib/Data/Holor.lean
Modified
Mathlib/Data/Int/Order/Basic.lean
Modified
Mathlib/Data/List/Chain.lean
Modified
Mathlib/Data/List/Cycle.lean
Modified
Mathlib/Data/List/Nodup.lean
Modified
Mathlib/Data/List/ToFinsupp.lean
Modified
Mathlib/Data/Multiset/Basic.lean
Modified
Mathlib/Data/MvPolynomial/Basic.lean
Modified
Mathlib/Data/MvPolynomial/CommRing.lean
Modified
Mathlib/Data/MvPolynomial/Equiv.lean
Modified
Mathlib/Data/MvPolynomial/Monad.lean
Modified
Mathlib/Data/MvPolynomial/Variables.lean
Modified
Mathlib/Data/Nat/Choose/Multinomial.lean
Modified
Mathlib/Data/Nat/Defs.lean
Modified
Mathlib/Data/Nat/Factorization/PrimePow.lean
Modified
Mathlib/Data/Nat/Multiplicity.lean
Modified
Mathlib/Data/Nat/Prime.lean
Modified
Mathlib/Data/Nat/Squarefree.lean
Modified
Mathlib/Data/Polynomial/AlgebraMap.lean
Modified
Mathlib/Data/Polynomial/Coeff.lean
Modified
Mathlib/Data/Polynomial/Degree/CardPowDegree.lean
Modified
Mathlib/Data/Polynomial/Degree/Definitions.lean
modified
theorem
Polynomial.leadingCoeff_ne_zero
Modified
Mathlib/Data/Polynomial/Degree/Lemmas.lean
Modified
Mathlib/Data/Polynomial/Derivative.lean
Modified
Mathlib/Data/Polynomial/EraseLead.lean
Modified
Mathlib/Data/Polynomial/FieldDivision.lean
Modified
Mathlib/Data/Polynomial/HasseDeriv.lean
Modified
Mathlib/Data/Polynomial/Inductions.lean
Modified
Mathlib/Data/Polynomial/Laurent.lean
Modified
Mathlib/Data/Polynomial/Lifts.lean
Modified
Mathlib/Data/Polynomial/Monic.lean
Modified
Mathlib/Data/Polynomial/RingDivision.lean
Modified
Mathlib/Data/Rat/Lemmas.lean
Modified
Mathlib/Data/Rat/Order.lean
Modified
Mathlib/Data/Real/Basic.lean
Modified
Mathlib/Data/Real/EReal.lean
Modified
Mathlib/Data/Real/Irrational.lean
Modified
Mathlib/Data/Real/NNReal.lean
Modified
Mathlib/Data/Real/Pi/Wallis.lean
Modified
Mathlib/Data/Set/Basic.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/Data/Set/Pairwise/Basic.lean
Modified
Mathlib/Data/Set/Pointwise/SMul.lean
Modified
Mathlib/Data/Set/Prod.lean
Modified
Mathlib/Data/Sum/Interval.lean
Modified
Mathlib/Data/Sym/Basic.lean
Modified
Mathlib/Data/Sym/Sym2.lean
Modified
Mathlib/Data/Vector/Basic.lean
Modified
Mathlib/Data/ZMod/Basic.lean
Modified
Mathlib/Dynamics/Ergodic/Conservative.lean
Modified
Mathlib/FieldTheory/IsAlgClosed/Classification.lean
Modified
Mathlib/FieldTheory/KrullTopology.lean
Modified
Mathlib/FieldTheory/KummerExtension.lean
Modified
Mathlib/FieldTheory/RatFunc.lean
Modified
Mathlib/Geometry/Euclidean/Circumcenter.lean
Modified
Mathlib/GroupTheory/Exponent.lean
Modified
Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
Modified
Mathlib/GroupTheory/Index.lean
Modified
Mathlib/GroupTheory/Order/Min.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Factors.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Type.lean
Modified
Mathlib/GroupTheory/Perm/List.lean
Modified
Mathlib/GroupTheory/Perm/Sign.lean
Modified
Mathlib/GroupTheory/Perm/Support.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Alternating.lean
Modified
Mathlib/GroupTheory/SpecificGroups/KleinFour.lean
Modified
Mathlib/GroupTheory/Subgroup/Basic.lean
Modified
Mathlib/GroupTheory/Submonoid/Operations.lean
Modified
Mathlib/GroupTheory/Torsion.lean
Modified
Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/FinsuppVectorSpace.lean
Modified
Mathlib/LinearAlgebra/Lagrange.lean
Modified
Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
Modified
Mathlib/LinearAlgebra/Matrix/IsDiag.lean
Modified
Mathlib/LinearAlgebra/Matrix/LDL.lean
Modified
Mathlib/LinearAlgebra/Matrix/Transvection.lean
Modified
Mathlib/LinearAlgebra/Multilinear/Basic.lean
Modified
Mathlib/LinearAlgebra/Projectivization/Independence.lean
Modified
Mathlib/LinearAlgebra/Ray.lean
Modified
Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/Vandermonde.lean
Modified
Mathlib/Logic/Basic.lean
Modified
Mathlib/Logic/Encodable/Basic.lean
Modified
Mathlib/Logic/Nontrivial/Basic.lean
Modified
Mathlib/Logic/Nontrivial/Defs.lean
Modified
Mathlib/MeasureTheory/Covering/Besicovitch.lean
Modified
Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
Modified
Mathlib/MeasureTheory/Covering/Differentiation.lean