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.
feat(NormedSpace/Basic): add dist_smul_add_one_sub_smul_le (#9982) From sphere-eversion (slightly golfed); I'm just upstreaming it.