OAI/NumberTheory/CubicMoment/Transform/MetaplecticForwardCompletion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact forward completion over a finite primary box. This identity allows the long inverse divisors to be collected by their actual product.

  1. theorem OAI.CubicFirstMoment.metaplectic_forward_completion line 12