The ℤ√d model for the Bareiss elimination

The computable model of the quadratic extensions ℤ√d. The elimination runs on ℤ√d values. Accepted entries are ⟨a, b⟩ literals, √d, or integers evaluated from norm_num.

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 its value. The entry is a ⟨re, im⟩ literal, √d itself, or an entry without √d content, which norm_num evaluates.

Equations

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

def Mathlib.Tactic.Echelon.zsqrtdOps (d : ℤ) : RingOps (ℤ√d)

The arithmetic of ℤ√d, with exact division by conjugation.

Equations

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

def Mathlib.Tactic.Echelon.zsqrtdModel {u : Lean.Level} (α : Q(Type u)) (dQ : Q(ℤ)) (d : ℤ) : Model α

The ℤ√d model of the ring α, which reduces to Zsqrtd dQ. The elimination runs on ℤ√d values. d is the value of the integer literal dQ.

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.