OAI/Combinatorics/MatchingPSD/Involutions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingSmoothing.eigen_add_commuting line 13
2. lemma OAI.MatchingSmoothing.eigen_sub_commuting line 19
3. lemma OAI.MatchingSmoothing.simultaneous_sign_eigenvector_on line 25
4. lemma OAI.MatchingSmoothing.simultaneous_sign_eigenvector line 70
5. lemma OAI.MatchingSmoothing.simultaneous_sign_eigenvector_preserving line 79
6. lemma OAI.MatchingSmoothing.independent_eigenprofiles line 109
7. lemma OAI.MatchingSmoothing.binomial_le_finrank_of_eigenvector line 123
8. lemma OAI.MatchingSmoothing.binomial_le_finrank_of_eigenvector_mem line 155