Polynomial.IsEisensteinAt P

Stream: mathlib4

[BANGJI HU]

any suggestion？

import Mathlib

set_option linter.unusedVariables false

open Polynomial

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

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

/-- The natural degree of P(x) is 10 -/
lemma P_natDegree : P.natDegree = 10 := by rw [P];compute_degree!

lemma P_nezero : P ≠ 0 :=
  ne_zero_of_natDegree_gt (n := 0) (by norm_num [P_natDegree])

lemma P_leadingCoeff : P.leadingCoeff = 4 := by rw [leadingCoeff, P_natDegree, P];simp

lemma P_coeff0 : P.coeff 0 = -18 := by rw [P]; simp

lemma P_coeff1 : P.coeff 1 = 24 := by rw [P];simp

lemma P_coeff3 : P.coeff 3 = -9 := by rw [P];simp

lemma eqq (p : ℕ) (hp : Nat.Prime p) (h_p_dvd_3 : p ∣ 3) : p = 3 := by
  have h3_prime : Nat.Prime 3 := by norm_num
  rw [← Nat.prime_dvd_prime_iff_eq hp h3_prime]
  exact h_p_dvd_3

theorem P_not_eisenstein_criterion_alt : ∀ (p : ℕ) [hp1: Fact p.Prime], ¬ Polynomial.IsEisensteinAt P (Ideal.span ({↑p} : Set ℤ)) := by
  intro p hp_inst
  let p' : ℤ := p
  -- Define the principal ideal generated by p'
  let 𝓟 : Ideal ℤ := Ideal.span {p'}
  let hp := hp_inst.out
  intro h_eisenstein
  -- Extract the three conditions from Eisenstein's criterion
  have h_mem_all : ∀ {n}, n < P.natDegree → P.coeff n ∈ 𝓟 := h_eisenstein.mem
  have h_not_mem : P.coeff 0 ∉ 𝓟^2 := h_eisenstein.not_mem
  -- Show that p' divides the constant term (coeff 0)
  have h_p_dvd_coeff0 : p' ∣ P.coeff 0 := by
    rw [← Ideal.mem_span_singleton]
    apply h_mem_all
    rw [P_natDegree]; norm_num
  -- Show that p' divides the coefficient of x (coeff 1)
  have h_p_dvd_coeff1 : p' ∣ P.coeff 1 := by
    rw [← Ideal.mem_span_singleton]
    apply h_mem_all (by rw [P_natDegree]; norm_num : 1 < P.natDegree)
  -- Show that p' divides the coefficient of x^3 (coeff 3)
  have h_p_dvd_coeff3 : p' ∣ P.coeff 3 := by
    rw [← Ideal.mem_span_singleton]
    apply h_mem_all
    rw [P_natDegree]; norm_num
  -- Substitute the actual coefficient values
  rw [P_coeff0] at h_p_dvd_coeff0
  rw [P_coeff1] at h_p_dvd_coeff1
  rw [P_coeff3] at h_p_dvd_coeff3
  -- Convert the divisibility conditions to natural numbers
  have h_p_dvd_18 : p ∣ 18 := by
    rw [Int.dvd_neg] at h_p_dvd_coeff0
    exact Int.ofNat_dvd.mp h_p_dvd_coeff0
  have h_p_dvd_24 : p ∣ 24 := by
     exact Int.ofNat_dvd.mp h_p_dvd_coeff1
  have h_p_dvd_9 : p ∣ 9 := by
     rw [Int.dvd_neg] at h_p_dvd_coeff3
     exact Int.ofNat_dvd.mp h_p_dvd_coeff3
  -- Compute GCDs to narrow down possible p values
  have h_gcd_24_18 : Nat.gcd 24 18 = 6 := by norm_num
  have h_gcd_9_6 : Nat.gcd 9 6 = 3 := by norm_num
  -- Show that p divides the GCD of 9 and the GCD of 24 and 18
  have h_p_dvd_gcd : p ∣ Nat.gcd 9 (Nat.gcd 24 18) := by
    apply Nat.dvd_gcd
    · exact h_p_dvd_9
    · apply Nat.dvd_gcd
      · exact h_p_dvd_24
      · exact h_p_dvd_18
  -- Conclude that p must be 3
  have h_p_eq_3 : p = 3 := by
    rw [h_gcd_24_18, h_gcd_9_6] at h_p_dvd_gcd
    exact eqq p hp h_p_dvd_gcd
  -- Check the non-membership condition for p = 3
  rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton] at h_not_mem
  rw [P_coeff0] at h_not_mem
  have h_p'_eq_3 : p' = (3 : ℤ) := by
    exact congrArg Int.ofNat h_p_eq_3
  rw [h_p'_eq_3] at h_not_mem
  norm_num at h_not_mem

[Antoine Chambert-Loir]

What do you wish to achieve?