mathlib

21581937 - feat(topology/instances/matrix): add topological/continuous instances (#14202)

feat(topology/instances/matrix): add topological/continuous instances (#14202) For completeness, `has_continuous_add` and `topological_add_group` instances are added to matrices, as pi types already have these. Additionally, `has_continuous_const_smul` and `has_continuous_smul` matrix instances have been made more generic, allowing differing index types. Co-authored-by: Aron Erben <aron.erben@econ.uzh.ch>