## Stream: new members

### Topic: irreduciable

#### Artizuiala G. (Mar 22 2022 at 13:17):

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?

Last updated: Dec 20 2023 at 11:08 UTC