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.checkDecideEq {u : Lean.Level} (α : Q(Type u)) (rα : Q(CommRing «$α»)) : Lean.MetaM Bool

Check whether the kernel can reduce decide ((2 : α) ≠ 0) to a boolean result (would be false in characteristic 2). Synthesizing the Decidable instance alone does not settle this, since types such as ℝ have classical instances defined for them. This check tests 2 against 0 (instead of 1), because some rings might have decidable equality facts between 0 and 1, but not for general entries against 0.

Equations

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

def Mathlib.Tactic.Echelon.normNumCertifier {u : Lean.Level} (α : Q(Type u)) : EntryCertifier α

norm_num's core as an entry certifier.

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.