Commit 2024-03-20 20:37 d8258805

View on Github →

chore(HomOrthogonal): fix Fintype/Finite (#11539)

Estimated changes

Modified Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean

modified theorem CategoryTheory.HomOrthogonal.equiv_of_iso

modified theorem CategoryTheory.HomOrthogonal.matrixDecomposition_comp

modified theorem CategoryTheory.HomOrthogonal.matrixDecomposition_id