OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootIwahoriDomain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The integral Iwahori normalizer sends the actual root-cover fundamental domain to another fundamental domain of the same subgroup.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootIwahoriImage_fundamental line 11