def Hex.FactorTactic.proveFpIrreducible (tactic : String) (p : Nat) [ZMod64.Bounds p] (hpt : Nat.isPrimeTrial p = true) (pE boundsE fE : Lean.Expr) : Lean.MetaM Lean.Expr

Constructs the proof emitted by irreducibility for f : FpPoly p: returns the proof of Hex.FpPoly.Irreducible f as a raw Expr over reified literal data.

Equations

• One or more equations did not get rendered due to their size.

def Hex.FactorTactic.elabIrreducibilityFp (tactic : String) (p : Nat) (pE boundsE fE : Lean.Expr) : Lean.MetaM Lean.Expr

Elaborate irreducibility f for f : FpPoly p.

Equations

• One or more equations did not get rendered due to their size.

def Hex.FactorTactic.elabIrreducibilityArgument (stx t : Lean.Syntax) (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Elaborate an irreducibility argument and produce the proof, selecting to extensions for non-FpPoly input types.

Equations

• One or more equations did not get rendered due to their size.

def Hex.FactorTactic.irreducibilityTerm : Lean.ParserDescr

irreducibility f elaborates to a proof that f is irreducible (Hex.FpPoly.Irreducible f for f : FpPoly p; extensions add further input types).

Equations

• One or more equations did not get rendered due to their size.

def Hex.FactorTactic.elabIrreducibility : Lean.Elab.Term.TermElab

Term elaborator for irreducibility f: runs the Rabin test in compiled code and returns the checked irreducibility proof term.

Equations

• One or more equations did not get rendered due to their size.

def Hex.FactorTactic.goalIrredFp (goal : Lean.MVarId) : Lean.Elab.Tactic.TacticM Bool

Try to close a goal of the form Hex.FpPoly.Irreducible e natively; return false when the goal has a different shape.

Equations

• One or more equations did not get rendered due to their size.

def Hex.FactorTactic.irreducibilityTac : Lean.ParserDescr

Tactic forms of irreducibility: bare irreducibility closes a goal of the form … .Irreducible e; irreducibility f adds the proof as this; irreducibility h : f names it h.

Equations

• One or more equations did not get rendered due to their size.

def Hex.FactorTactic.evalIrreducibilityTac : Lean.Elab.Tactic.Tactic

Tactic elaborator for irreducibility: closes an Irreducible goal, or adds the proof to the local context under this or a caller-chosen name.

Equations

• One or more equations did not get rendered due to their size.