OAI/Topology/ArtinGroups/Harmonic/CartanCommutingZero.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourceCartan_commuting_zero line 15
2. lemma OAI.HarmonicArtin.harmonic_block_eq line 20
3. lemma OAI.HarmonicArtin.sourceCosetVector_block line 44
4. lemma OAI.HarmonicArtin.sourceCosetProduct_open_left line 66
5. lemma OAI.HarmonicArtin.sourceCosetProduct_open_right line 94