irreduciable

Stream: new members

[Artizuiala G.]

I'm trying to prove that f(x) = x² + 1 is irreducible over 𝔽₃
the mathematic prove I have is:

f(0)=1, f(1)=2, f(2)=2²+1=2 in 𝔽₃, all ≠ 0 (mod 3)
So, f(x) = x² + 1 is irreducible over 𝔽₃ since it doesn't have a root in 𝔽₃

I'm thinking to set the theorem that if f has degree 2 or 3 and has no root in given field, then f is irreduciableBut I need to prove it.
So, insteand, I using the given structure of irreduciable to set my statement. so far, I have:

import tactic
import data.zmod.algebra
import data.polynomial.basic

noncomputable theory

open_locale polynomial

open polynomial

def f : (zmod 3)[X] := X^2 + 1
/-
f(0)=1, f(1)=2, f(2)=2²+1=2 in 𝔽₃, all ≠ 0 (mod 3)
So, f(x) = x² + 1 is irreducible over 𝔽₃ since it doesn't have a root in 𝔽₃
-/
example : irreducible f :=
{ not_unit' :=
  begin
     intro,
     cases ᾰ,
     sorry,
  end,

is_unit_or_is_unit' :=
  begin
    intros a b,
    intro h1,
    sorry,
  end}

But I have no ideal how to do next.
What should I do for this? any hint?