Commit 2023-07-05 13:45 6a3e867e
View on Github →feat(Analysis.Seminorm): remove useless assumption (#5734)
This removes a chance to infer an argument, but I think that's a fairly good use case for using the new named arguments, because adding (r := _) to specify a radius feels completely right.