OAI/NumberTheory/CubicMoment/Estimates/PrimitiveCharacterStar.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Conjugation preserves the actual finite conductor. For a cubic character, its square is precisely its conjugate, including the zero extension.

  1. lemma OAI.CubicFirstMoment.ResidueCharacterInduces.star line 10
  2. lemma OAI.CubicFirstMoment.PrimitiveResidueCharacter.star line 18
  3. lemma OAI.CubicFirstMoment.cubic_residue_character_sq_eq_star line 24
  4. lemma OAI.CubicFirstMoment.star_residue_character_ne_one line 33
  5. lemma OAI.CubicFirstMoment.star_residue_character_units line 40
  6. lemma OAI.CubicFirstMoment.residueIdealChar_cubic_square line 46