Commit 2024-05-28 16:14 3185f99d

View on Github →

chore: Do not import order theory in Data.Int.Cast.Lemmas (#13305) Split off the lemmas about OrderedRing from Data.Int.Cast.Lemmas to a new file Algebra.Order.Ring.Cast.

Estimated changes

added theorem Int.cast_abs
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_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_strictMono
added theorem ofDual_intCast
added theorem ofLex_intCast
added theorem toDual_intCast
added theorem toLex_intCast
deleted theorem Int.cast_abs
added theorem Int.cast_eq_one
added theorem Int.cast_eq_zero
added theorem Int.cast_inj
added theorem Int.cast_injective
deleted theorem Int.cast_le
deleted theorem Int.cast_lt
deleted theorem Int.cast_lt_zero
deleted theorem Int.cast_max
deleted theorem Int.cast_min
deleted theorem Int.cast_mono
deleted theorem Int.cast_natAbs
added theorem Int.cast_ne_one
added theorem Int.cast_ne_zero
deleted theorem Int.cast_nonneg
deleted theorem Int.cast_nonpos
deleted theorem Int.cast_one_le_of_pos
deleted theorem Int.cast_pos
deleted theorem Int.cast_strictMono
modified theorem Int.coe_castAddHom
deleted theorem ofDual_intCast
deleted theorem ofLex_intCast
deleted theorem toDual_intCast
deleted theorem toLex_intCast
deleted theorem Int.cast_eq_one
deleted theorem Int.cast_eq_zero
deleted theorem Int.cast_inj
deleted theorem Int.cast_injective
deleted theorem Int.cast_ne_one
deleted theorem Int.cast_ne_zero