Theorem CategoryTheory.HomOrthogonal.matrixDecomposition_id

Modification history

2024-03-20 20:37
Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
chore(HomOrthogonal): fix `Fintype`/`Finite` (#11539)
Modified CategoryTheory.HomOrthogonal.matrixDecomposition_idView on Github →
2023-05-10 13:30
Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
feat: port CategoryTheory.Preadditive.HomOrthogonal (#3734)
Added CategoryTheory.HomOrthogonal.matrixDecomposition_idView on Github →