Commit 2022-11-20 10:32 bff54619

View on Github →

feat: port Algebra.Order.Hom.Basic (#627) mathlib3 sha: 17ef379e997badd73e5eabb4d38f11919ab3c4b3

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Hom/Basic.lean

added theorem le_map_add_map_div

added theorem le_map_div_add_map_div

added theorem le_map_div_mul_map_div

added theorem le_map_mul_map_div