irrducible poly

Stream: mathlib4

[vxctyxeha]

any lemma can be used from mathlib to proved that x^2+pi is irreducible in R?

[Michał Staromiejski]

Could not find anything direct but you can use docs#Polynomial.irreducible_of_degree_le_three_of_not_isRoot to prove.

[vxctyxeha]

import Mathlib
open Subgroup Finset


open Polynomial
open Real
theorem pi_poly_irreducible_R : Irreducible (X^2 + C π : Polynomial ℝ) := by

   apply  irreducible_of_degree_le_three_of_not_isRoot

[vxctyxeha]

@Michał StaromiejskiSo that's not on R.

[Michał Staromiejski]

Of course it is not direct but you can use it to prove your goal. In your attempt, after apply you have two unsolved goals to prove:

case hdeg
⊢ (X ^ 2 + C π).natDegree ∈ Icc 1 3
case hnot
⊢ ∀ (x : ℝ), ¬(X ^ 2 + C π).IsRoot x

This should be easy.

[vxctyxeha]

Michał Staromiejski said:

Of course it is not direct but you can use it to prove your goal. In your attempt, after apply you have two unsolved goals to prove:

case hdeg
⊢ (X ^ 2 + C π).natDegree ∈ Icc 1 3
case hnot
⊢ ∀ (x : ℝ), ¬(X ^ 2 + C π).IsRoot x

This should be easy.

that is not on R so you cant apply

[Michał Staromiejski]

So what is R then? I think you mean reals?

[vxctyxeha]

is not irreducible over R

[vxctyxeha]

@Michał Staromiejski

import Mathlib
open Subgroup Finset


open Polynomial
open Real
theorem pi_poly_irreducible_R : Irreducible (X^2 + C π : Polynomial ℝ) := by

   refine (irreducible_of_degree_le_three_of_not_isRoot ?_ ?_).mpr ?_

[Michał Staromiejski]

Sorry, I don't understand your question, can you please be more specific?

[vxctyxeha]

proved that x^2+pi is irreducible in R

[Michał Staromiejski]

I still don't get your question, sorry.

[Riccardo Brasca]

vxctyxeha said:

Michał Staromiejski

import Mathlib
open Subgroup Finset


open Polynomial
open Real
theorem pi_poly_irreducible_R : Irreducible (X^2 + C π : Polynomial ℝ) := by

   refine (irreducible_of_degree_le_three_of_not_isRoot ?_ ?_).mpr ?_

Finishing this proof is rather easy. You can use compute_degree! to show that the degree is 2, and then simp will surely finish the job. The other goal is easy to, we know that x^2 is nonnegative and that pi is positive.

[vxctyxeha]

how to prove that root=0

import Mathlib
open Subgroup Finset
open Polynomial
open Real

lemma p_natDegree : ( X^2 + C π : Polynomial ℝ).natDegree = 2 := by compute_degree!
theorem pi_poly_irreducible_R : Irreducible (X^2 + C π : Polynomial ℝ) := by
  refine (Monic.irreducible_iff_roots_eq_zero_of_degree_le_three ?_ ?_ ?_).mpr ?_
  apply monic_X_pow_add_C (n := 2) -- Apply lemma for Monic Xⁿ + C c
  simp
  rw [p_natDegree]
  simp
  sorry

[Michał Staromiejski]

If you use docs#Polynomial.irreducible_of_degree_le_three_of_not_isRoot as I suggested in the beginning, you don't need to worry about Monic part. You started good, but you had two goals to solve left.

[Michał Staromiejski]

BTW, the goal about degrees can by done by simp.

[Jz Pan]

Maybe you can prove a more general result: if a quadratic polynomial over an ordered field has discriminant < 0, then it is irreducible.