OAI/RepresentationTheory/RowColumn/HookIsometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RowColumn.exists_hook_isometry line 13
2. lemma OAI.RowColumn.hook_copy_projection_intertwines line 52
3. lemma OAI.RowColumn.isotypic_filter_copy_projection line 87