Commit 2022-12-14 12:30 5c6a9da4

View on Github →

feat: port Data.Int.Cast.Lemmas (#995) fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Estimated changes

deleted theorem Int.cast_mul
added theorem AddMonoidHom.ext_int
added def Int.castAddHom
added def Int.castRingHom
added theorem Int.cast_abs
added theorem Int.cast_add_hom_int
added theorem Int.cast_comm
added theorem Int.cast_commute
added theorem Int.cast_ite
added theorem Int.cast_le
added theorem Int.cast_lt
added theorem Int.cast_lt_zero
added theorem Int.cast_max
added theorem Int.cast_min
added theorem Int.cast_mono
added theorem Int.cast_mul
added theorem Int.cast_natAbs
added theorem Int.cast_nonneg
added theorem Int.cast_nonpos
added theorem Int.cast_one_le_of_pos
added theorem Int.cast_pos
added theorem Int.cast_ring_hom_int
added theorem Int.cast_strict_mono
added theorem Int.coe_cast_add_hom
added theorem Int.coe_cast_ring_hom
added theorem Int.coe_int_dvd
added theorem Int.coe_nat_pos
added theorem Int.coe_nat_succ_pos
added theorem Int.commute_cast
added def Int.ofNatHom
added theorem MonoidHom.ext_int
added theorem MonoidHom.ext_mint
added theorem Pi.coe_int
added theorem Pi.int_apply
added theorem RingHom.eq_int_cast'
added theorem RingHom.ext_int
added theorem eq_int_cast'
added theorem eq_int_cast
added theorem ext_int'
added theorem map_int_cast
added theorem of_dual_int_cast
added theorem of_lex_int_cast
added theorem to_dual_int_cast
added theorem to_lex_int_cast