irreducible

Stream: new members

[Notification Bot]

Artizuiala G. has marked this topic as unresolved.

[Artizuiala G.]

but I still need to prove these two things:

example : irreducible f :=
{ not_unit' :=
  begin
     intro,
     cases ᾰ,
     sorry,
  end,

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

to prove my lemma:

lemma irreducible_of_not_root {F : Type*} [field F] (f : F[X]) (hfdeg : f.degree = 2 ∨ f.degree = 3) (hf : ∀ x, f.eval x ≠ 0) :
  irreducible f :=
begin
  cases hfdeg,
  -- f.degree = 2 case
  { fconstructor,
    -- goal 1: ¬is_unit f
    { intro,
      cases ᾰ,
      sorry,},
    -- goal 2: ∀ (a b : F[X]), f = a * b → is_unit a ∨ is_unit b
    { intros a b h1,
      sorry,},
  },
  -- f.degree = 3 case
  {sorry},
end

any suggestion?

[Ruben Van de Velde]

What's the pen and paper proof you're formalising?

[Ruben Van de Velde]

The first one I've found online assumes f is reducible and derives a contradiction; you can use the by_contra tactic for that