Commit 2025-02-21 15:59 3dc98f10

View on Github →

chore: deprecate Finite.cast_card_eq_mk (#22161) (the noshake is necessary)

Estimated changes

Modified Mathlib/Data/Finite/Card.lean

deleted theorem Finite.cast_card_eq_mk

Modified Mathlib/Deprecated/Cardinal/Finite.lean

Modified scripts/noshake.json