Hello, I am looking for formalization of induced matrix norms. Could someone please guide me to the formalization in either mathcomp or some other source ?
Last updated: Feb 08 2023 at 07:02 UTC