Commit 2025-04-26 03:37 a91fc5ca

View on Github →

feat(Algebra/Order/Field/Defs): generalize lemmas (#24377) ... from linear ordered semifields to (commutative) groups with zero.

Estimated changes

deleted theorem inv_mul_le_one
deleted theorem inv_mul_left_le
deleted theorem inv_mul_right_le
deleted theorem le_inv_mul_left
deleted theorem le_inv_mul_right
deleted theorem le_mul_div_mul_left
deleted theorem le_mul_div_mul_right
deleted theorem le_mul_inv_left
deleted theorem le_mul_inv_right
deleted theorem mul_div_mul_left_le
deleted theorem mul_div_mul_right_le
deleted theorem mul_inv_le_one
deleted theorem mul_inv_left_le
deleted theorem mul_inv_right_le
added theorem inv_mul_le_one
added theorem inv_mul_left_le
added theorem inv_mul_right_le
added theorem le_inv_mul_left
added theorem le_inv_mul_right
added theorem le_mul_div_mul_left
added theorem le_mul_div_mul_right
added theorem le_mul_inv_left
added theorem le_mul_inv_right
added theorem mul_div_mul_left_le
added theorem mul_div_mul_right_le
added theorem mul_inv_le_one
added theorem mul_inv_left_le
added theorem mul_inv_right_le