HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

theory of diagonal matrices #1977

Closed Alizter closed 4 months ago

Alizter commented 4 months ago

We write down the property of being a diagonal matrix, show that this is a hprop (how nice), and show that standard opertions on matrices preserve diagonal matrices. This lets us define the subring of diagonal matrices of the ring of matrices.

Depends on: