Commit 2023-11-26 04:56 c159834a

View on Github →

fix: patch for std4#203 (more sub lemmas for Nat) (#6216)

Estimated changes

Modified Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean

Modified Mathlib/Analysis/BoundedVariation.lean

Modified Mathlib/Control/Random.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Fin/Interval.lean

Modified Mathlib/Data/Nat/Basic.lean

modified theorem Nat.add_succ_sub_one

modified theorem Nat.succ_add_sub_one

Modified Mathlib/Data/Nat/Factorial/Cast.lean

Modified Mathlib/Data/Nat/Order/Basic.lean

Modified Mathlib/Data/Polynomial/Derivative.lean

Modified Mathlib/Data/Stream/Init.lean

Modified Mathlib/Data/ZMod/Basic.lean

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

Modified Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

Modified Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

Modified Mathlib/NumberTheory/Wilson.lean

Modified Mathlib/Order/JordanHolder.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

Modified Mathlib/RingTheory/Polynomial/Hermite/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Vieta.lean

Modified lake-manifest.json