Commit 2025-10-16 02:52 68304f20

View on Github →

chore(SetTheory): deprecate mk_multiset_of_countable and iSup_succ. remove cast_succ. (#28488)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Finsupp.lean

deleted theorem Cardinal.mk_multiset_of_countable

Modified Mathlib/SetTheory/Ordinal/Family.lean

deleted theorem Ordinal.iSup_succ

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean