mathlib documentation

topology.algebra.matrix

Topological properties of matrices #

This file is a place to collect topological results about matrices.

Main definitions: #

@[protected, instance]
def matrix.topological_space {ι : Type u_1} {k : Type u_2} [topological_space k] :
Equations
theorem continuous_det {ι : Type u_1} {k : Type u_2} [topological_space k] [fintype ι] [decidable_eq ι] [comm_ring k] [topological_ring k] :