The rational model for the Bareiss elimination

The computable model of literals expressible in ℚ. It is the fallback model the tactic uses when no other model matches the ring.

def Mathlib.Tactic.Echelon.evalRatEntry (charZero : Bool) (e : Lean.Expr) : Lean.MetaM ℚ

Data-only evaluation of a matrix entry to its rational value via norm_num. Fraction values are accepted only in characteristic zero.

Equations

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

def Mathlib.Tactic.Echelon.mkIntNumeral {u : Lean.Level} (α : Q(Type u)) (i : ℤ) : Lean.MetaM Q(«$α»)

Build the numeral of an integer in α: mkNumeral on the absolute value, negated if i is negative.

Equations

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

def Mathlib.Tactic.Echelon.ratModel {u : Lean.Level} (α : Q(Type u)) (rα : Q(CommRing «$α»)) : Lean.MetaM (Model ℤ)

The rational model.

Equations

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