OAI/NumberTheory/CubicMoment/Estimates/CoprimeResidueLift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lift a prime-to-modulus residue while avoiding any prescribed nonzero factor. This keeps the actual cubic-character witness away from the cube part of its numerator.

  1. lemma OAI.CubicFirstMoment.isCoprime_of_residue_congr line 11
  2. theorem OAI.CubicFirstMoment.exists_coprime_residue_lift line 18

    Source documentation

    Every residue prime to q has a representative prime to q*c.

    theorem exists_coprime_residue_lift {q a c : Eisenstein}
    (hc : c ≠ 0) (ha : IsCoprime q a) :
    ∃ x : Eisenstein, q ∣ x-a ∧ IsCoprime (q*c) x := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein