OAI/Topology/ArtinGroups/ParabolicIntersections/TreeInvariantTranslate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Equivariance of invariant vertex sets under subgroup conjugation.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.conjugate_preserves_image line 9
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.not_mem_image_of_smul_eq line 17