OAI/Topology/ArtinGroups/Harmonic/FusionFold.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.fusionFold line 14
2. def OAI.HarmonicArtin.fusionUnfoldedCartan line 17
3. def OAI.HarmonicArtin.fusionFoldedCartan line 22
4. lemma OAI.HarmonicArtin.fusion_intertwining line 25
5. lemma OAI.HarmonicArtin.fusionUnfoldedCartan_symm line 46
6. lemma OAI.HarmonicArtin.fusionUnfoldedCartan_off line 55
7. def OAI.HarmonicArtin.fusionD0 line 61
8. lemma OAI.HarmonicArtin.fusion_pairing line 63
9. lemma OAI.HarmonicArtin.fusionD0_pos line 76
10. lemma OAI.HarmonicArtin.harmonic_posDef_of_strict_rows line 82
11. lemma OAI.HarmonicArtin.fusion_positive_definite line 120