OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootWeylInvolution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Involutivity of the actual conjugated inversion, on both the arithmetic root subgroup and positive-height points.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeylConjugate_matrix line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeylConjugate_involutive line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeylElement_inversion line 43
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeylPoint_intertwines line 57
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeylPoint_involutive line 66