I can't find a way to transform
`| x * y | into
`|x| * `|y| when both x and y have type R, and R is a realType (using mathcomp-analysis, but I think this is a mathcomp issue).
isn’t it normrM ?
I was sure to have tried and failed it, but now it does work. I must be too tired.
I could find normrM because I was using the wrong search pattern, and normrM was not an obvious name for me, because of the trailing r.
Last updated: Feb 08 2023 at 07:02 UTC