Commit 2023-11-05 13:30 cdcad962

View on Github →

fix: patch for std4#195 (more succ/pred lemmas for Nat) (#6203)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Intervals.lean

Modified Mathlib/Algebra/CharP/Basic.lean

Modified Mathlib/Algebra/GeomSum.lean

Modified Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Modified Mathlib/Combinatorics/Additive/Behrend.lean

Modified Mathlib/Combinatorics/Hall/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Finset/Powerset.lean

Modified Mathlib/Data/Finset/Sort.lean

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/Nat/Basic.lean

Modified Mathlib/Data/Nat/Digits.lean

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/Data/Polynomial/Derivative.lean

Modified Mathlib/Data/Polynomial/EraseLead.lean

Modified Mathlib/Data/Polynomial/Module.lean

Modified Mathlib/Init/Data/Nat/Lemmas.lean

Modified Mathlib/Init/Meta/WellFoundedTactics.lean

modified theorem Nat.zero_lt_one_add

Modified Mathlib/NumberTheory/Multiplicity.lean

Modified Mathlib/Probability/Martingale/Upcrossing.lean

Modified Mathlib/Probability/StrongLaw.lean

Modified Mathlib/RingTheory/IntegralClosure.lean

Modified Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean

Modified Mathlib/RingTheory/Polynomial/Bernstein.lean

Modified Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

Modified Mathlib/Testing/SlimCheck/Gen.lean

Modified Mathlib/Util/DischargerAsTactic.lean

Modified lake-manifest.json

Modified test/lift.lean