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: Oct 13 2024 at 01:02 UTC