Commit 2024-10-23 04:26 77ffa0d4

View on Github →

chore(SetTheory/Cardinal/Basic): deprecate duplicate Nat.cast lemmas (#17850) Spotted thanks to #17827.

Estimated changes

modified theorem Cardinal.natCast_inj
modified theorem Cardinal.natCast_injective
modified theorem Cardinal.natCast_le
modified theorem Cardinal.natCast_lt
modified theorem Cardinal.natCast_pow
deleted theorem Cardinal.pow_cast_right
added theorem Cardinal.power_natCast