Commit 2024-08-09 11:40 dc29147d

View on Github →

chore (Algebra.Order.Group.Int): split file into unbundled and bundled ordered algebra (#15069) All but ~5 lines of this file did not require bundled ordered algebra classes. We split them off into Algebra.Order.Group.Unbundled.Int leaving the LinearOrderedAddCommGroup instance.

Estimated changes

deleted theorem Int.abs_ediv_le_abs
deleted theorem Int.abs_eq_natAbs
deleted theorem Int.abs_le_one_iff
deleted theorem Int.abs_lt_one_iff
deleted theorem Int.abs_natCast
deleted theorem Int.abs_sign_of_nonzero
deleted theorem Int.emod_abs
deleted theorem Int.emod_lt
deleted theorem Int.le_self_sq
deleted theorem Int.natAbs_abs
deleted theorem Int.natAbs_le_self_sq
deleted theorem Int.natAbs_sub_pos_iff
deleted theorem Int.natCast_natAbs
deleted theorem Int.natCast_strictMono
deleted theorem Int.one_le_abs
deleted theorem Int.sign_mul_abs
deleted theorem zpow_abs_eq_one
added theorem Int.abs_ediv_le_abs
added theorem Int.abs_eq_natAbs
added theorem Int.abs_le_one_iff
added theorem Int.abs_lt_one_iff
added theorem Int.abs_natCast
added theorem Int.emod_abs
added theorem Int.emod_lt
added theorem Int.le_self_sq
added theorem Int.natAbs_abs
added theorem Int.natAbs_le_self_sq
added theorem Int.natAbs_sub_pos_iff
added theorem Int.natCast_natAbs
added theorem Int.natCast_strictMono
added theorem Int.one_le_abs
added theorem Int.sign_mul_abs
added theorem zpow_abs_eq_one