Commit 2023-05-10 13:30 9912e05d

View on Github →

feat: port CategoryTheory.Preadditive.HomOrthogonal (#3734)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean

added theorem CategoryTheory.HomOrthogonal.eq_zero

added theorem CategoryTheory.HomOrthogonal.equiv_of_iso

added theorem CategoryTheory.HomOrthogonal.matrixDecomposition_comp

added theorem CategoryTheory.HomOrthogonal.matrixDecomposition_id

added def CategoryTheory.HomOrthogonal