The ℤ√d model for the Bareiss elimination

The computable model of the quadratic extensions ℤ√d: the elimination runs on ℤ√d values with the ring's own arithmetic, with exact division by conjugation. Entries are ⟨a, b⟩ literals, √d, or numerals.

def Mathlib.Tactic.Echelon.evalInt (e : Lean.Expr) : Lean.MetaM ℤ

Evaluate an entry or component of the ℤ√d model to an integer, via norm_num.

Equations

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

def Mathlib.Tactic.Echelon.evalZsqrtdEntry (d : ℤ) (e : Lean.Expr) : Lean.MetaM (ℤ√d)

Evaluate a ℤ√d entry to a ℤ√d value: a ⟨a, b⟩ literal, √d itself, or an entry without √d content evaluating through norm_num.

Equations

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

def Mathlib.Tactic.Echelon.zsqrtdProducer (dQ : Q(ℤ)) (d : ℤ) : Producer

The ℤ√d model, for d the value of the integer literal dQ: the elimination runs on ℤ√d values with the ring's own arithmetic.

Equations

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

def Mathlib.Tactic.Echelon.zsqrtdExt : BareissExt

The ℤ√d model registration: handles Zsqrtd d for an integer literal d.

Equations

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