PrimaryPrimePNTProofSplitting.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Rational splitting and the literal primary Eisenstein primes.

lemma OAI.CubicFirstMoment.normNat_natCast line 12
lemma OAI.CubicFirstMoment.isUnit_iff_normNat_eq_one line 18
lemma OAI.CubicFirstMoment.prime_of_normNat_prime line 22
lemma OAI.CubicFirstMoment.primary_natCast_of_mod_one line 31
lemma OAI.CubicFirstMoment.primaryPrime_rational_below line 40
Source documentation
Every primary prime lies over a rational prime, and its norm has degree at most two.
```
lemma primaryPrime_rational_below {z : Eisenstein} (hz : primaryPrime z) :
    ∃ p : ℕ, p.Prime ∧ z ∣ (p : Eisenstein) ∧
      (normNat z = p ∨ normNat z = p ^ 2) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.normNat
lemma OAI.CubicFirstMoment.primaryPrime_norm_prime_mod_one line 67
Source documentation
If its norm is a rational prime, that prime is in the split class.
```
lemma primaryPrime_norm_prime_mod_one {z : Eisenstein} (hz : primaryPrime z)
    (hn : (normNat z).Prime) : normNat z % 3 = 1 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.normNat
lemma OAI.CubicFirstMoment.not_prime_natCast_of_mod_one line 74
Source documentation
In the split residue class the rational prime is reducible in the Eisenstein ring.
```
lemma not_prime_natCast_of_mod_one {p : ℕ} (hp : p.Prime) (hmod : p % 3 = 1) :
    ¬ Prime (p : Eisenstein) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
theorem OAI.CubicFirstMoment.exists_primaryPrime_norm_of_mod_one line 124
Source documentation
Each split rational prime is the norm of an actual primary prime.
```
theorem exists_primaryPrime_norm_of_mod_one {p : ℕ} (hp : p.Prime)
    (hmod : p % 3 = 1) : ∃ z : Eisenstein, primaryPrime z ∧ normNat z = p := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.normNat