Commit 2025-04-03 14:23 32c2cc01

View on Github →

chore: use full name for natCast, intCast, etc (#23563) This is not exhaustive, and only covers Irrational and FloorRing. Every renamed lemma has been deprecated.

Estimated changes

deleted theorem Int.ceil_add_int
added theorem Int.ceil_add_intCast
deleted theorem Int.ceil_add_nat
added theorem Int.ceil_add_natCast
deleted theorem Int.ceil_sub_int
added theorem Int.ceil_sub_intCast
deleted theorem Int.ceil_sub_nat
added theorem Int.ceil_sub_natCast
deleted theorem Int.floor_add_int
added theorem Int.floor_add_intCast
deleted theorem Int.floor_add_nat
added theorem Int.floor_add_natCast
added theorem Int.floor_intCast_add
deleted theorem Int.floor_int_add
added theorem Int.floor_natCast_add
deleted theorem Int.floor_nat_add
deleted theorem Int.floor_sub_int
added theorem Int.floor_sub_intCast
deleted theorem Int.floor_sub_nat
added theorem Int.floor_sub_natCast
modified theorem Int.floor_sub_one
deleted theorem Int.fract_add_int
added theorem Int.fract_add_intCast
deleted theorem Int.fract_add_nat
added theorem Int.fract_add_natCast
modified theorem Int.fract_add_one
added theorem Int.fract_intCast_add
deleted theorem Int.fract_int_add
deleted theorem Int.fract_mul_nat
added theorem Int.fract_mul_natCast
added theorem Int.fract_natCast_add
deleted theorem Int.fract_nat_add
modified theorem Int.fract_one_add
deleted theorem Int.fract_sub_int
added theorem Int.fract_sub_intCast
deleted theorem Int.fract_sub_nat
added theorem Int.fract_sub_natCast
modified theorem Int.fract_sub_one
deleted theorem Nat.ceil_add_nat
added theorem Nat.ceil_add_natCast
deleted theorem Nat.floor_add_nat
added theorem Nat.floor_add_natCast
deleted theorem Nat.floor_div_nat
added theorem Nat.floor_div_natCast
deleted theorem Nat.floor_sub_nat
added theorem Nat.floor_sub_natCast
deleted theorem Irrational.add_int
added theorem Irrational.add_intCast
deleted theorem Irrational.add_nat
added theorem Irrational.add_natCast
deleted theorem Irrational.add_rat
added theorem Irrational.add_ratCast
deleted theorem Irrational.div_int
added theorem Irrational.div_intCast
deleted theorem Irrational.div_nat
added theorem Irrational.div_natCast
deleted theorem Irrational.div_rat
added theorem Irrational.div_ratCast
added theorem Irrational.intCast_add
added theorem Irrational.intCast_div
added theorem Irrational.intCast_mul
added theorem Irrational.intCast_sub
deleted theorem Irrational.int_add
deleted theorem Irrational.int_div
deleted theorem Irrational.int_mul
deleted theorem Irrational.int_sub
deleted theorem Irrational.mul_int
added theorem Irrational.mul_intCast
deleted theorem Irrational.mul_nat
added theorem Irrational.mul_natCast
deleted theorem Irrational.mul_rat
added theorem Irrational.mul_ratCast
added theorem Irrational.natCast_add
added theorem Irrational.natCast_div
added theorem Irrational.natCast_mul
added theorem Irrational.natCast_sub
deleted theorem Irrational.nat_add
deleted theorem Irrational.nat_div
deleted theorem Irrational.nat_mul
deleted theorem Irrational.nat_sub
deleted theorem Irrational.of_add_int
deleted theorem Irrational.of_add_nat
deleted theorem Irrational.of_add_rat
deleted theorem Irrational.of_div_int
deleted theorem Irrational.of_div_nat
deleted theorem Irrational.of_div_rat
deleted theorem Irrational.of_int_add
deleted theorem Irrational.of_int_div
deleted theorem Irrational.of_int_mul
deleted theorem Irrational.of_int_sub
deleted theorem Irrational.of_mul_int
deleted theorem Irrational.of_mul_nat
deleted theorem Irrational.of_mul_rat
deleted theorem Irrational.of_nat_add
deleted theorem Irrational.of_nat_div
deleted theorem Irrational.of_nat_mul
deleted theorem Irrational.of_nat_sub
deleted theorem Irrational.of_rat_add
deleted theorem Irrational.of_rat_div
deleted theorem Irrational.of_rat_mul
deleted theorem Irrational.of_rat_sub
deleted theorem Irrational.of_sub_int
deleted theorem Irrational.of_sub_nat
deleted theorem Irrational.of_sub_rat
added theorem Irrational.ratCast_add
added theorem Irrational.ratCast_div
added theorem Irrational.ratCast_mul
added theorem Irrational.ratCast_sub
deleted theorem Irrational.rat_add
deleted theorem Irrational.rat_div
deleted theorem Irrational.rat_mul
deleted theorem Irrational.rat_sub
deleted theorem Irrational.sub_int
added theorem Irrational.sub_intCast
deleted theorem Irrational.sub_nat
added theorem Irrational.sub_natCast
deleted theorem Irrational.sub_rat
added theorem Irrational.sub_ratCast
deleted theorem irrational_add_int_iff
deleted theorem irrational_add_nat_iff
deleted theorem irrational_add_rat_iff
deleted theorem irrational_div_int_iff
deleted theorem irrational_div_nat_iff
deleted theorem irrational_div_rat_iff
deleted theorem irrational_int_add_iff
deleted theorem irrational_int_div_iff
deleted theorem irrational_int_mul_iff
deleted theorem irrational_int_sub_iff
deleted theorem irrational_mul_int_iff
deleted theorem irrational_mul_nat_iff
deleted theorem irrational_mul_rat_iff
deleted theorem irrational_nat_add_iff
deleted theorem irrational_nat_div_iff
deleted theorem irrational_nat_mul_iff
deleted theorem irrational_nat_sub_iff
deleted theorem irrational_rat_add_iff
deleted theorem irrational_rat_div_iff
deleted theorem irrational_rat_mul_iff
deleted theorem irrational_rat_sub_iff
deleted theorem irrational_sub_int_iff
deleted theorem irrational_sub_nat_iff
deleted theorem irrational_sub_rat_iff