mod3

Stream: mathlib4

[vxctyxeha]

tactic 'rewrite' failed, motive is not type correct:
fun _a => polya.natDegree + polyb.natDegree = _a
Error: application type mismatch
@ZMod.instField _a ⋯
argument

import Mathlib
open Polynomial
instance : Fact (Nat.Prime 3) := ⟨(by norm_num)⟩

theorem irreducible3 : Irreducible (X^3+2 * X + 1 : (ZMod 3)[X]) :=by
    refine (Monic.irreducible_iff_natDegree (by monicity!)).mpr ?_

    have : (X ^ 3 + 2*X  + 1 : (ZMod 3)[X]).natDegree = 3 := by compute_degree!
    constructor
    by_contra eq
    have : (X ^ 3 + 2*X + 1 : (ZMod 3)[X]).natDegree = (1 : (ZMod 3)[X]).natDegree := by rw [eq]
    -- but $1$ has degree $0$, contradiction
    have : (1 : (ZMod 3)[X]).natDegree = 0 := natDegree_one
    linarith
    intro polya polyb monica monicb fac
    have sum : polya.natDegree + polyb.natDegree = 3 := by rw [←this, ← fac, ← (Monic.natDegree_mul monica monicb)]

[Kevin Buzzard]

Your continual posting of low-effort questions, which many of us suspect correspond to asking for help on work which you are being paid for (which is why you post with an anonymous name) is pushing you quickly towards a suspension from this Zulip.