The rational model for the Bareiss elimination

The rational model of a ring: entries evaluate to rational numerals via norm_num, denominators are cleared by row scaling, and the elimination runs on integer values. It is the fallback model the tactic uses when no ring-specific 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.scaleRowsIntegral (ratRows : Array (Array ℚ)) : Array (Array ℤ) × Array ℕ

Scale each row by the lcm of its denominators to clear them. Returns the integer matrix together with the row scales, which are later folded back into L.

Equations

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

def Mathlib.Tactic.Echelon.restoreScaling (scales : Array ℕ) (d : BareissData ℤ) : BareissData ℤ

The restoration for scaleRowsIntegral: fold the row scales into the transform, scaling column j by the factor of the row that ends up in position j.

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.ratProducer (R : Lean.Expr) : Lean.MetaM Producer

The rational model of a ring: entries evaluate to rational numerals, denominators are cleared by row scaling, and the elimination runs on integer values. It applies to every ring, as the fallback model.

Equations

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