Commit 2024-02-13 19:40 9afd0027

View on Github →

chore: bump Std (#10482)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Multiset/Basic.lean

Modified Mathlib/Computability/Ackermann.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Multiset/Nodup.lean

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

Modified Mathlib/Data/Nat/Defs.lean

deleted theorem Nat.eq_of_le_of_lt_succ

deleted theorem Nat.eq_of_lt_succ_of_not_lt

deleted theorem Nat.exists_eq_add_of_le'

deleted theorem Nat.exists_eq_add_of_le

deleted theorem Nat.exists_eq_add_of_lt

deleted theorem Nat.mod_mod_of_dvd

Modified Mathlib/Data/Nat/Digits.lean

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

Modified Mathlib/Data/Nat/Pow.lean

deleted theorem Nat.pow_dvd_pow_iff_le_right'

deleted theorem Nat.pow_dvd_pow_iff_le_right

deleted theorem Nat.pow_dvd_pow_iff_pow_le_pow

deleted theorem Nat.pow_lt_pow_succ

Modified Mathlib/NumberTheory/Padics/Hensel.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified lake-manifest.json

Modified scripts/noshake.json