Commit 2026-10-23 15:44 64fa0ec7

View on Github ā†’

chore: rename coe_nat/nat_cast lemmas to natCast (#44825) This renames Lean 3 style coe_nat and nat_cast in lemma names about Nat.cast to natCast. šŸ¤– Generated with Claude Code

Estimated changes

deleted theorem Int.normalize_coe_nat
added theorem Int.normalize_natCast
deleted theorem Int.even_coe_nat
added theorem Int.even_natCast
deleted theorem MvPolynomial.C_eq_coe_nat
deleted theorem Int.coe_nat_two_pow_pred
deleted theorem Int.odd_coe_nat
added theorem Int.odd_natCast
added theorem RCLike.conj_natCast
deleted theorem RCLike.conj_nat_cast
deleted theorem Real.natCastle_toNNReal'
deleted theorem Int.bit_coe_nat
added theorem Int.bit_natCast
deleted theorem NNRat.toNNRat_coe_nat
added theorem NNRat.toNNRat_natCast
deleted theorem Cardinal.nat_coe_dvd_iff