The ℤ√d model for the Bareiss elimination

The computable model of the quadratic extensions ℤ√d. The elimination runs on Expr representing ⟨a, b⟩ literals with raw integer components. 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.intOfRawLit? (e : Lean.Expr) : Option ℤ

The integer of a raw literal Int.ofNat n or Int.negOfNat n.

Equations

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

def Mathlib.Tactic.Echelon.zsqrtdOfRawLit? (d : ℤ) (e : Lean.Expr) : Option (ℤ√d)

The value of a literal ⟨re, im⟩ : ℤ√d with raw integer components.

Equations

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

def Mathlib.Tactic.Echelon.mkZsqrtdRawLit (dQ : Q(ℤ)) {d : ℤ} (v : ℤ√d) : Q(ℤ√«$dQ»)

The literal that zsqrtdOfRawLit? reads back as v.

def Mathlib.Tactic.Echelon.zsqrtdModel (dQ : Q(ℤ)) (d : ℤ) : Model Lean.Expr

The ℤ√d model. The elimination runs on literals with raw integer components, computed with the arithmetic of ℤ√d. 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.