Commit 2024-01-09 09:25 e1b05c51

View on Github →

chore: Move Int and Nat cast lemmas (#9503) Part of #9411

Estimated changes

deleted theorem AddMonoidHom.apply_nat
deleted theorem Commute.cast_int_left
deleted theorem Commute.cast_int_mul_left
deleted theorem Commute.cast_int_mul_self
deleted theorem Commute.cast_int_right
deleted theorem Commute.cast_nat_mul_left
deleted theorem Commute.cast_nat_mul_self
deleted theorem Commute.self_cast_int_mul
deleted theorem Commute.self_cast_nat_mul
deleted theorem Int.cast_pow
deleted theorem Int.coe_nat_pow
deleted theorem Int.natAbs_pow
deleted theorem Int.ofAdd_mul
deleted theorem Int.toAdd_pow
deleted theorem Int.toAdd_zpow
deleted theorem MonoidHom.apply_mnat
deleted theorem MonoidHom.ext_mnat
deleted theorem Nat.cast_pow
deleted theorem Nat.ofAdd_mul
deleted theorem Nat.toAdd_pow
deleted def multiplesAddHom
deleted theorem multiplesAddHom_apply
deleted def multiplesHom
deleted theorem multiplesHom_apply
deleted theorem multiplesHom_symm_apply
deleted theorem nsmul_eq_mul'
deleted theorem nsmul_eq_mul
deleted theorem nsmul_one
modified theorem pow_eq
deleted def powersHom
deleted theorem powersHom_apply
deleted theorem powersHom_symm_apply
deleted def powersMulHom
deleted theorem powersMulHom_apply
deleted theorem powersMulHom_symm_apply
deleted theorem zsmul_eq_mul'
deleted theorem zsmul_eq_mul
deleted theorem zsmul_int_int
deleted theorem zsmul_int_one
deleted theorem zsmul_one
added theorem Int.cast_pow
added theorem Int.natAbs_pow
added theorem Int.ofAdd_mul
added theorem Int.toAdd_pow
added theorem Int.toAdd_zpow
added theorem zsmul_int_int
added theorem zsmul_int_one
added theorem Commute.cast_int_left
added theorem Commute.cast_int_right
modified def Int.castRingHom
modified theorem Int.cast_comm
modified theorem Int.cast_commute
modified theorem Int.coe_castRingHom
added theorem Int.coe_nat_pow
modified theorem Int.commute_cast
added theorem zsmul_eq_mul'
added theorem zsmul_eq_mul
added theorem zsmul_one
added theorem Nat.ofAdd_mul
added theorem Nat.toAdd_pow
added theorem AddMonoidHom.apply_nat
added theorem MonoidHom.apply_mnat
added theorem MonoidHom.ext_mnat
modified def Nat.castRingHom
modified theorem Nat.cast_mul
added theorem Nat.cast_pow
modified theorem Nat.coe_castRingHom
modified theorem Nat.coe_nat_dvd
added def multiplesAddHom
added theorem multiplesAddHom_apply
added def multiplesHom
added theorem multiplesHom_apply
added theorem nsmul_eq_mul'
added theorem nsmul_eq_mul
added theorem nsmul_one
added def powersHom
added theorem powersHom_apply
added theorem powersHom_symm_apply
added def powersMulHom
added theorem powersMulHom_apply