OAI/Topology/ArtinGroups/ParabolicIntersections/PointedCosetProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Pointed multiplicities on products of commuting standard cosets.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_open line 12
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_block line 18
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetProduct_open_left line 40
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetProduct_open_right line 68