Commit 2024-01-27 11:43 c8818ba7

View on Github →

feat(NormedSpace/Basic): add dist_smul_add_one_sub_smul_le (#9982) From sphere-eversion (slightly golfed); I'm just upstreaming it.

Estimated changes