nnnorm and complex

Stream: Is there code for X?

[Eric Rodriguez]

I found lemmata about nnnorm of complex numbers in the Wedderburn stuff, do people know where these should go? I can't seem to find anything to do with complex.*nnnorm using regex search

[Eric Wieser]

Probably right next to any lemmas about norm on complex numbers?

[Eric Rodriguez]

hmm, all I can sort of see is complex.norm_eq_abs. do you think I should stick it there?