polynomials123

Stream: mathlib4

[vxctyxeha]

typeclass instance problem is stuck, it is often due to metavariables
HSub ?m.15435[X] ℕ[X] ℤ?

import Mathlib
open Polynomial

noncomputable def f : Polynomial ℤ := X^3 + C 3 * X^2 - C 8

noncomputable def g : Polynomial ℤ := X^3 - C 3 * X - C 6

theorem f_transform_eq_g : Polynomial.eval (X - C 1) f = g := by
  rw [f, g]
  simp [eval_add, eval_sub, eval_mul, eval_pow, eval_X, eval_C]
  ring

[vxctyxeha]

the same happens when i switch to \R

import Mathlib
open Polynomial

noncomputable def f : Polynomial ℤ := X^3 + C 3 * X^2 - C 8

noncomputable def g : Polynomial ℤ := X^3 - C 3 * X - C 6

theorem f_transform_eq_g : Polynomial.eval (X - C 1 : ℝ) f = p := by
  rw [f, g]
  simp [eval_add, eval_sub, eval_mul, eval_pow, eval_X, eval_C]
  ring

[Ilmārs Cīrulis]

import Mathlib
open Polynomial

noncomputable def f : Polynomial ℤ := X^3 + C 3 * X^2 - C 8

noncomputable def g : Polynomial ℤ := X^3 - C 3 * X - C 6

theorem f_transform_eq_g x: eval (x - 1) f = eval x g:= by
  rw [f, g]
  simp
  ring

or maybe

import Mathlib
open Polynomial

noncomputable def f : Polynomial ℤ := X^3 + C 3 * X^2 - C 8

noncomputable def g : Polynomial ℤ := X^3 - C 3 * X - C 6

theorem f_transform_eq_g: comp f (X - C 1) = g := by
  rw [f, g]
  simp
  ring

[Ilmārs Cīrulis]

Sorry for no explanation, too sleepy.

[vxctyxeha]

Hello everyone, for a polynomial I can't use Eisenstein's discriminant to prove that it is reducible over Q, so I directly deformed and substituted x-1 so that it can use Eisenstein's discriminant, but how can I use my lemma to prove that my original polynomial is irreducible@Ilmārs Cīrulis

import Mathlib
open Polynomial

attribute [local simp] coeff_X

/--
The original cubic polynomial from the question: f(x) = x³ + 3x² - 8 -/
noncomputable def f : Polynomial ℤ := X^3 + C 3 * X^2 - C 8
/-- A transformed version of f, obtained by substituting (x-1):p(x) = f(x-1) = x³ - 3x - 6 -/
noncomputable def p : Polynomial ℤ := X^3 - C 3 * X - C 6
/- We prove that f(x-1) = p(x) -/
lemma f_transform_eq_g x : eval (x - 1) f = eval x p := by rw [f, p];simp;ring
/-- The natural degree of p(x) is 3 (highest power with non-zero coefficient) -/
lemma p_natDegree : p.natDegree = 3 := by rw [p];   compute_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])
/-- The leading coefficient (of x³) is 1 -/
lemma p_leadingCoeff : p.leadingCoeff = 1 := by rw [leadingCoeff, p_natDegree, p];simp
/-- The support (set of exponents with non-zero coefficients) is {0,1,3} -/
lemma p_support : p.support = {0, 1, 3} := by
  ext i
  constructor
  . intro hi
    contrapose! hi
    rcases lt_or_le 3 i with h | h
    . have : p.coeff i = 0 := coeff_eq_zero_of_natDegree_lt (by rwa [p_natDegree])
      simpa using this
    . interval_cases i <;> simp at hi ; simp [p]
  . intro hi
    simp at hi
    casesm* _ ∨ _
    all_goals simp [hi, p]

/--
Main theorem: p(x) is irreducible over ℤ (and thus ℚ) via Eisenstein's criterion

This uses the prime 3 to satisfy Eisenstein's conditions:
1. 3 divides all non-leading coefficients (-3, -6)
2. 3² = 9 does not divide the constant term (-6)
3. The leading coefficient is 1 (not divisible by 3)
-/
theorem irreducible_of_eis : Irreducible p := by
  apply irreducible_of_eisenstein_criterion (P := Ideal.span {3})  -- Use prime 3
  -- Prove ⟨3⟩ is a prime ideal
  . rw [Ideal.span_singleton_prime (by norm_num)]; norm_num  -- 3 is prime
  -- Prove 3 doesn't divide leading coefficient (1)
  . rw [Ideal.mem_span_singleton, p_leadingCoeff]; norm_num  -- 3 ∤ 1
  -- Prove 3 divides all other coefficients (0, 1, 3)
  . intro n hn
    rw [degree_eq_natDegree p_nezero, p_natDegree] at hn
    norm_cast at hn
    rw [Ideal.mem_span_singleton]
    interval_cases n <;> simp [p] ; norm_num  -- Check n=0,1,2 cases
  -- Prove p is non-constant
  . rw [degree_eq_natDegree p_nezero, p_natDegree]; norm_num  -- deg=3 ≠ 0
  -- Prove 3²=9 doesn't divide constant term
  . rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton]
    simp [p]
    norm_num-- 9 ∤ 6
  -- Prove p is primitive (gcd of coefficients is 1)
  . rw [isPrimitive_iff_content_eq_one, content, p_support]
    simp [p]

theorem f_irreducible_int : Irreducible f := by
  sorry

[Ilmārs Cīrulis]

To summon me, you have to add space before @.

Anyway, looking into it.

[vxctyxeha]

import Mathlib
open Polynomial

lemma taylor_irr {R : Type*} [CommRing R] (p : R[X]) (t : R): Irreducible p ↔ Irreducible ((taylor t) p) := by
  let f : R[X] ≃+* R[X] := {
    (Polynomial.eval₂RingHom C (X + C t)) with
    invFun := taylor (-t)
    left_inv := by
      intro q; dsimp
      rw [show (eval₂ C _ q) = (taylor t) q by rfl, taylor_taylor]; simp
    right_inv := by
      intro q; dsimp
      rw [show (eval₂ C _ _) = (taylor t) ((taylor (-t)) q) by rfl, taylor_taylor]; simp}
  rw [show (taylor t) p = f p by rfl, MulEquiv.irreducible_iff]
/--

[vxctyxeha]

@Ilmārs Cīrulis check this out

import Mathlib
open Polynomial

attribute [local simp] coeff_X

/--
The original cubic polynomial from the question: f(x) = x³ + 3x² - 8 -/
noncomputable def f : Polynomial ℤ := X^3 + C 3 * X^2 - C 8
/-- A transformed version of f, obtained by substituting (x-1):p(x) = f(x-1) = x³ - 3x - 6 -/
noncomputable def p : Polynomial ℤ := X^3 - C 3 * X - C 6
/- We prove that f(x-1) = p(x) -/
lemma f_transform_eq_g x : eval (x - 1) f = eval x p := by rw [f, p];simp;ring
/-- The natural degree of p(x) is 3 (highest power with non-zero coefficient) -/
lemma p_natDegree : p.natDegree = 3 := by rw [p];   compute_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])
/-- The leading coefficient (of x³) is 1 -/
lemma p_leadingCoeff : p.leadingCoeff = 1 := by rw [leadingCoeff, p_natDegree, p];simp
/-- The support (set of exponents with non-zero coefficients) is {0,1,3} -/
lemma p_support : p.support = {0, 1, 3} := by
  ext i
  constructor
  . intro hi
    contrapose! hi
    rcases lt_or_le 3 i with h | h
    . have : p.coeff i = 0 := coeff_eq_zero_of_natDegree_lt (by rwa [p_natDegree])
      simpa using this
    . interval_cases i <;> simp at hi ; simp [p]
  . intro hi
    simp at hi
    casesm* _ ∨ _
    all_goals simp [hi, p]

lemma taylor_irr {R : Type*} [CommRing R] (p : R[X]) (t : R): Irreducible p ↔ Irreducible ((taylor t) p) := by
  let f : R[X] ≃+* R[X] := {
    (Polynomial.eval₂RingHom C (X + C t)) with
    invFun := taylor (-t)
    left_inv := by
      intro q; dsimp
      rw [show (eval₂ C _ q) = (taylor t) q by rfl, taylor_taylor]; simp
    right_inv := by
      intro q; dsimp
      rw [show (eval₂ C _ _) = (taylor t) ((taylor (-t)) q) by rfl, taylor_taylor]; simp}
  rw [show (taylor t) p = f p by rfl, MulEquiv.irreducible_iff]

/--
Main theorem: p(x) is irreducible over ℤ (and thus ℚ) via Eisenstein's criterion

This uses the prime 3 to satisfy Eisenstein's conditions:
1. 3 divides all non-leading coefficients (-3, -6)
2. 3² = 9 does not divide the constant term (-6)
3. The leading coefficient is 1 (not divisible by 3)
-/
theorem irreducible_of_eis : Irreducible p := by
  apply irreducible_of_eisenstein_criterion (P := Ideal.span {3})  -- Use prime 3
  -- Prove ⟨3⟩ is a prime ideal
  . rw [Ideal.span_singleton_prime (by norm_num)]; norm_num  -- 3 is prime
  -- Prove 3 doesn't divide leading coefficient (1)
  . rw [Ideal.mem_span_singleton, p_leadingCoeff]; norm_num  -- 3 ∤ 1
  -- Prove 3 divides all other coefficients (0, 1, 3)
  . intro n hn
    rw [degree_eq_natDegree p_nezero, p_natDegree] at hn
    norm_cast at hn
    rw [Ideal.mem_span_singleton]
    interval_cases n <;> simp [p] ; norm_num  -- Check n=0,1,2 cases
  -- Prove p is non-constant
  . rw [degree_eq_natDegree p_nezero, p_natDegree]; norm_num  -- deg=3 ≠ 0
  -- Prove 3²=9 doesn't divide constant term
  . rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton]
    simp [p]
    norm_num-- 9 ∤ 6
  -- Prove p is primitive (gcd of coefficients is 1)
  . rw [isPrimitive_iff_content_eq_one, content, p_support]
    simp [p]

theorem f_irreducible_int : Irreducible f := by
  have h_f_eq_taylor_p : f = taylor 1 p := by
    simp [f, p, taylor_apply] -- Expand definitions using taylor_apply lemma
    ring -- Verify polynomial equality algebraically
  rw [h_f_eq_taylor_p]
  refine (taylor_irr p 1).mp ?_
  exact irreducible_of_eis
  ```

[Ilmārs Cīrulis]

Congrats! :)

[vxctyxeha]

what about the irrducible over Q

[Ilmārs Cīrulis]

There is rational root theorem here
I'm learning how to use it, for now.