OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeLowerChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The lower-unipotent chart covers precisely the cosets whose bottom right entry is a unit at the chosen prime.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeLowerChart_covers line 10