Commit 2023-01-04 12:39 127c1f98

View on Github →

feat: port data.rat.cast (#1261)

Estimated changes

added theorem MulOpposite.op_ratCast
added def Rat.castHom
added theorem Rat.cast_abs
added theorem Rat.cast_add
added theorem Rat.cast_bit0
added theorem Rat.cast_bit1
added theorem Rat.cast_coe_int
added theorem Rat.cast_coe_nat
added theorem Rat.cast_comm
added theorem Rat.cast_commute
added theorem Rat.cast_div
added theorem Rat.cast_eq_id
added theorem Rat.cast_eq_zero
added theorem Rat.cast_hom_rat
added theorem Rat.cast_id
added theorem Rat.cast_inj
added theorem Rat.cast_injective
added theorem Rat.cast_inv
added theorem Rat.cast_inv_int
added theorem Rat.cast_inv_nat
added theorem Rat.cast_le
added theorem Rat.cast_lt
added theorem Rat.cast_lt_zero
added theorem Rat.cast_max
added theorem Rat.cast_min
added theorem Rat.cast_mk
added theorem Rat.cast_mk_of_ne_zero
added theorem Rat.cast_mono
added theorem Rat.cast_mul
added theorem Rat.cast_ne_zero
added theorem Rat.cast_neg
added theorem Rat.cast_nonneg
added theorem Rat.cast_nonpos
added theorem Rat.cast_one
added theorem Rat.cast_pos
added theorem Rat.cast_pos_of_pos
added theorem Rat.cast_pow
added theorem Rat.cast_strictMono
added theorem Rat.cast_sub
added theorem Rat.cast_zero
added theorem Rat.cast_zpow
added theorem Rat.coe_cast_hom
added theorem Rat.commute_cast
added theorem Rat.preimage_cast_Icc
added theorem Rat.preimage_cast_Ici
added theorem Rat.preimage_cast_Ico
added theorem Rat.preimage_cast_Iic
added theorem Rat.preimage_cast_Iio
added theorem Rat.preimage_cast_Ioc
added theorem Rat.preimage_cast_Ioi
added theorem Rat.preimage_cast_Ioo
added theorem RingHom.ext_rat
added theorem eq_ratCast
added theorem map_ratCast