Commit 2023-12-08 22:28 d76f1524

View on Github →

fix: patch for std4#197 (More add lemmas for Nat) (#6202)

Estimated changes

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Control/Fix.lean

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/Data/List/Sort.lean

Modified Mathlib/Data/Nat/Bitwise.lean

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

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

Modified Mathlib/Data/Nat/Pairing.lean

Modified Mathlib/Data/Polynomial/Derivative.lean

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

Modified Mathlib/Init/Meta/WellFoundedTactics.lean

deleted theorem Nat.lt_add_left

Modified Mathlib/Logic/Equiv/Fin.lean

modified theorem finAddFlip_apply_mk_left

Modified Mathlib/NumberTheory/Bernoulli.lean

Modified Mathlib/NumberTheory/Multiplicity.lean

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

Modified Mathlib/RingTheory/PowerSeries/Derivative.lean

Modified Mathlib/Tactic/NormNum/Prime.lean

Modified lake-manifest.json

Modified lakefile.lean