Commit 2023-09-07 09:49 f0c7f6d3

View on Github →

chore: split Data.Rat.Cast (#7001)

Estimated changes

added def Rat.castHom
added theorem Rat.cast_add
added theorem Rat.cast_bit0
added theorem Rat.cast_bit1
added theorem Rat.cast_div
added theorem Rat.cast_eq_zero
added theorem Rat.cast_inj
added theorem Rat.cast_injective
added theorem Rat.cast_inv
added theorem Rat.cast_mk
added theorem Rat.cast_mul
added theorem Rat.cast_ne_zero
added theorem Rat.cast_pow
added theorem Rat.cast_sub
added theorem Rat.cast_zpow
added theorem Rat.coe_cast_hom
deleted def Rat.castHom
deleted theorem Rat.cast_abs
deleted theorem Rat.cast_add
deleted theorem Rat.cast_bit0
deleted theorem Rat.cast_bit1
deleted theorem Rat.cast_div
deleted theorem Rat.cast_eq_zero
deleted theorem Rat.cast_hom_rat
deleted theorem Rat.cast_inj
deleted theorem Rat.cast_injective
deleted theorem Rat.cast_inv
deleted theorem Rat.cast_le
deleted theorem Rat.cast_lt
deleted theorem Rat.cast_lt_zero
deleted theorem Rat.cast_max
deleted theorem Rat.cast_min
deleted theorem Rat.cast_mk
deleted theorem Rat.cast_mono
deleted theorem Rat.cast_mul
deleted theorem Rat.cast_ne_zero
deleted theorem Rat.cast_nonneg
deleted theorem Rat.cast_nonpos
deleted theorem Rat.cast_pos
deleted theorem Rat.cast_pos_of_pos
deleted theorem Rat.cast_pow
deleted theorem Rat.cast_strictMono
deleted theorem Rat.cast_sub
deleted theorem Rat.cast_zpow
deleted theorem Rat.coe_cast_hom
deleted theorem Rat.preimage_cast_Icc
deleted theorem Rat.preimage_cast_Ici
deleted theorem Rat.preimage_cast_Ico
deleted theorem Rat.preimage_cast_Iic
deleted theorem Rat.preimage_cast_Iio
deleted theorem Rat.preimage_cast_Ioc
deleted theorem Rat.preimage_cast_Ioi
deleted theorem Rat.preimage_cast_Ioo
added theorem Rat.cast_abs
added theorem Rat.cast_hom_rat
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_mono
added theorem Rat.cast_nonneg
added theorem Rat.cast_nonpos
added theorem Rat.cast_pos
added theorem Rat.cast_pos_of_pos
added theorem Rat.cast_strictMono
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