OAI/NumberTheory/CubicMoment/Angular/AngularSquareCompletion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The square of a fixed nonzero angular character is completed through its own primitive conductor. The omitted Euler factors are retained.

  1. lemma OAI.CubicFirstMoment.angularResidueIdealChar_square line 11
  2. lemma OAI.CubicFirstMoment.AngularUnitCompatible.square line 19
  3. theorem OAI.CubicFirstMoment.angular_square_primitive_completion line 28