OAI/NumberTheory/CubicMoment/Estimates/BalancedSmallPartTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Balanced full-factor estimates on the original, possibly ramified rows.

  1. theorem OAI.CubicFirstMoment.balanced_smalltwist_smooth_fiber_power line 12
  2. theorem OAI.CubicFirstMoment.balanced_smalltwist_smooth_partition_power line 68