Commit 2024-09-02 07:30 00df099f

View on Github →

feat: ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖ when ‖a‖ ≤ 1 (#16318) This inequality is particularly useful when c = 1 and ‖a‖ = ‖b‖ = 1 as it then shows that chord length is a metric on the unit circle. From LeanAPAP

Estimated changes