Commit 2024-09-23 09:33 09c50fb8

View on Github →

feat: a * a⁻¹ ≤ 1 (#17023) From LeanAPAP

Estimated changes

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_inv_left
added theorem le_mul_inv_right
added theorem mul_inv_le_one
added theorem mul_inv_left_le
added theorem mul_inv_right_le