OAI/NumberTheory/DukePrimeDegree/Geometry/MeasureConjugation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Conjugation of the actual measure stabilizer

Right translation conjugates stabilizers in the opposite direction. These identities apply to arbitrary measures and do not assume that the translating element preserves the measure.

  1. lemma OAI.DukePrimeDegree.map_rightAction_mul line 19
  2. lemma OAI.DukePrimeDegree.map_rightAction_injective line 28
  3. lemma OAI.DukePrimeDegree.mem_invariantRightSubgroup_map_iff line 36