Commit 2026-09-24 09:55 e18afff3

View on Github →

chore(Algebra/Order/Hom/Basic): split file by imports (#43109) I ran intro trouble importing Algebra/Order/Hom/Basic into Algebra/Order/BigOperators/Group/Finset (which has assert_not_exists Ring) in order to prove subadditivity for finite sums. The file Algebra/Order/Hom/Basic is already organized into a basic section, a group norms section, and a ring norms section, so splitting the file along those divisions seemed simplest.

Estimated changes

deleted theorem abs_sub_map_le_div
deleted theorem le_map_add_map_div'
deleted theorem map_div_le_add
deleted theorem map_div_rev
deleted theorem map_eq_zero_iff_eq_one
deleted theorem map_inv_mul
deleted theorem map_ne_zero_iff_ne_one
deleted theorem map_pos_of_ne_one
added theorem abs_sub_map_le_div
added theorem le_map_add_map_div'
added theorem map_div_le_add
added theorem map_div_rev
added theorem map_eq_zero_iff_eq_one
added theorem map_inv_mul
added theorem map_ne_zero_iff_ne_one
added theorem map_pos_of_ne_one