f.IsWeaklyEisensteinAt

Stream: mathlib4

[BANGJI HU]

Hello, I am trying to prove that a polynomial does not satisfy the Eisenstein criterion. My question now is how to express the statement. The proof of the problem is in the code below, but I did not use f.IsWeaklyEisensteinAt.

import Mathlib

/-!

# Nonexistence of a Prime Satisfying Specific Conditions

This file proves that there exists no prime number p satisfying all of the following conditions:

1. p divides 9, 24, and 18
2. p does not divide 4
3. p² does not divide 18

-/

/--
Any prime number dividing 3 must be equal to 3.

**Parameters:**
- `p`: A natural number
- `hp`: Proof that `p` is prime
- `h_p_dvd_3`: Proof that `p` divides 3

**Returns:**
- A proof that `p = 3`
-/
lemma eqq (p : ℕ) (hp : Nat.Prime p) (h_p_dvd_3 : p ∣ 3) : p = 3 := by
  -- First show that 3 is prime
  have h3_prime : Nat.Prime 3 := by norm_num

  -- Use the theorem that for primes p and q, p ∣ q ↔ p = q
  rw [← Nat.prime_dvd_prime_iff_eq hp h3_prime]

  -- Apply our hypothesis that p divides 3
  exact h_p_dvd_3

/--
No prime number satisfies all the specified conditions:
1. Divides 9, 24, and 18
2. Does not divide 4
3. Has its square not dividing 18

**Proof Strategy:**
1. Assume such a prime p exists (for contradiction)
2. Show p must divide gcd(9, gcd(24, 18)) = 3
3. Use lemma `eqq` to conclude p = 3
4. Show p = 3 contradicts the third condition (9 does divide 18)
-/
theorem no_prime_satisfies_conditions : ¬∃ p : ℕ, p.Prime ∧ (p ∣ 9 ∧ p ∣ 24 ∧ p ∣ 18) ∧ ¬(p ∣ 4) ∧ ¬(p ^ 2 ∣ 18) := by
  -- Proof by contradiction: assume such a prime exists
  rintro ⟨p, hp, h1, h2, h3⟩

  -- Compute gcd(9, gcd(24, 18)) = 3
  have h_gcd : Nat.gcd 9 (Nat.gcd 24 18) = 3 := by norm_num

  -- p must divide the gcd since it divides all three numbers
  have h_p_dvd_gcd : p ∣ Nat.gcd 9 (Nat.gcd 24 18) :=
    Nat.dvd_gcd h1.1 (Nat.dvd_gcd h1.2.1 h1.2.2)

  -- Since gcd is 3 and p is prime, p must be 3
  have h_p_eq_3 : p = 3 := by
    rw [h_gcd] at h_p_dvd_gcd
    exact eqq p hp h_p_dvd_gcd

  -- Substitute p = 3 into the remaining conditions
  rw [h_p_eq_3] at h3

  -- 3² = 9 does divide 18 (violates condition 3)
  have h_9_dvd_18 : 9 ∣ 18 := by norm_num

  -- This contradicts our assumption
  contradiction

[BANGJI HU]

import Mathlib


open Polynomial

attribute [local simp] coeff_X  -- Simplify coefficient lookups for X^n

/-- The polynomial we want to analyze: 8x³ + 6x² - 9x + 24 -/
noncomputable def   P : ℤ[X] :=C 4 * X^10 - C 9 * X^3 + C 24 * X - C 18

/-- The natural degree of p(x) is 3 (highest power with non-zero coefficient) -/
lemma P_natDegree : P.natDegree = 10 := by
  rw [P]          -- Expand the definition of p
  compute_degree! -- Automatically compute the degree

/-- p(x) is not the zero polynomial -/
lemma P_nezero : P ≠ 0 :=
  ne_zero_of_natDegree_gt (n := 0) (by norm_num [P_natDegree])  -- Since degree > 0, it's non-zero

/-- The leading coefficient (of x³) is 8 -/
lemma P_leadingCoeff : P.leadingCoeff = 4:= by
  rw [leadingCoeff, P_natDegree, P]  -- Unfold definitions
  simp  -- Simplify the expression

/-- The constant term (coefficient of x⁰) is 24 -/
lemma P.coeff0 : P.coeff 0 = -18 := by
  rw [P]  -- Expand p
  simp    -- Simplify



theorem P_not_eisenstein_criterion :
    ∀ (p : ℕ) [hp : Fact p.Prime], ¬ Polynomial.IsEisensteinAt P (Ideal.span ({↑p} : Set ℤ)) := by
    intro p hp_inst
    let p' : ℤ := p -- Cast p to integer for ideal generation
    let 𝓟 : Ideal ℤ := Ideal.span {p'} -- Define the ideal
    let hp := hp_inst.out -- Get the primality proof from the instance
    intro h_eisenstein
    rcases hp.eq_two_or_odd with rfl | h_odd
    have h_leading := h_eisenstein.leading -- leadingCoeff P ∉ 𝓟
    rw [P_leadingCoeff] at h_leading
    dsimp [𝓟] at h_leading -- 4 ∉ span {2}
    rw [Ideal.mem_span_singleton] at h_leading -- ¬ (2 ∣ 4)
    apply h_leading -- This is the contradiction
    contradiction