Topological properties of matrices #
This file is a place to collect topological results about matrices.
Main definitions: #
continuous_det: the determinant is continuous over a topological ring.
@[protected, instance]
def
matrix.topological_space
{ι : Type u_1}
{k : Type u_2}
[topological_space k] :
topological_space (matrix ι ι k)
Equations
theorem
continuous_det
{ι : Type u_1}
{k : Type u_2}
[topological_space k]
[fintype ι]
[decidable_eq ι]
[comm_ring k]
[topological_ring k] :