Commit 2023-02-27 14:49 8266a4c2

View on Github →

forward port changes to Algebra.Order.Hom.Basic (#2401) This forward ports changes to this file from [mathlib3#16919](https://github.com/leanprover-community/mathlib/pull/16919). This does not address the other files in that PR, but #1238 is open to address those. This is being PR'ed separately so that work on Analysis.Normed.Group.Seminorm can continue (#2400).

Estimated changes

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_ne_zero_iff_ne_one
added theorem map_pos_of_ne_one