PrimaryPrimePNTProofFibers.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact fibers above split rational primes, and the quadratic-norm remainder.

lemma OAI.CubicFirstMoment.normNat_intCast line 10
lemma OAI.CubicFirstMoment.primaryPrime_ne_conjugate_of_prime_norm line 17
lemma OAI.CubicFirstMoment.pnt_primaryPrime_eq_or_conjugate_of_norm_eq line 36
lemma OAI.CubicFirstMoment.primaryPrime_normFiber_card_le_two line 48
theorem OAI.CubicFirstMoment.primaryPrime_normFiber_card_eq_two line 71
Source documentation
Exactly two primary primes lie above each split rational prime.
```
theorem primaryPrime_normFiber_card_eq_two {p : ℕ} (hp : p.Prime)
    (hmod : p % 3 = 1) {X : ℝ} (hpX : (p : ℝ) ≤ X) :
    ((primeCutoff X).filter (fun z => normNat z = p)).card = 2 := by
…
```
Mentions: OAI.CubicFirstMoment.primeCutoff, OAI.CubicFirstMoment.normNat
lemma OAI.CubicFirstMoment.primaryPrime_norm_square_of_not_prime line 91
Source documentation
Every other norm is the square of a rational prime.
```
lemma primaryPrime_norm_square_of_not_prime {z : Eisenstein} (hz : primaryPrime z)
    (hn : ¬ (normNat z).Prime) :
    ∃ p : ℕ, p.Prime ∧ normNat z = p ^ 2 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.normNat