OAI/NumberTheory/CubicMoment/Angular/AngularBalancedFullRows.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Collection over the second conductor variable, with literal row fibers.

  1. theorem OAI.CubicFirstMoment.balanced_angular_smalltwist_log_pair_power line 13
  2. theorem OAI.CubicFirstMoment.balanced_angular_smalltwist_pair_power line 50