OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootBruhatOperators.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The nonzero Bruhat branches act on actual global sections by the reciprocal root parameter and its cubic symbol. The zero branch retains the literal squared-prime dilation.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_translated_global line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_global_zero line 28