Stream: math-comp users

Topic: norm and multiplication


view this post on Zulip 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).

view this post on Zulip Reynald Affeldt (May 31 2021 at 15:31):

isn’t it normrM ?

view this post on Zulip 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.

view this post on Zulip 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: Feb 08 2023 at 07:02 UTC