Yves Bertot (May 31 2021 at 15:15): Yves Bertot (May 31 2021 at 15:15):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).
Reynald Affeldt (May 31 2021 at 15:31):isn’t it normrM ?
Yves Bertot (May 31 2021 at 15:44):I was sure to have tried and failed it, but now it does work. I must be too tired.
Yves Bertot (May 31 2021 at 15:58):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: Sep 15 2024 at 13:02 UTC