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: Apr 18 2024 at 09:02 UTC