OAI/NumberTheory/CubicMoment/Angular/AngularKummerAlgebra.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The literal angular cubic character, with the argument order of the cubic residue symbol. Only multiplicativity in the prime variable is used; the fixed angular factor is not duplicated in the numerator variable.

  1. def OAI.CubicFirstMoment.angularCubicSymbol line 12
  2. lemma OAI.CubicFirstMoment.angularCubicSymbol_mul_lower line 15
  3. lemma OAI.CubicFirstMoment.angularCubicSymbol_norm_le_one line 22