Documentation

Mathlib.Tactic.NormRank

eval_rank: rank of matrix literals by Bareiss elimination #

This module defines the eval_rank tactic and the norm_rank simproc, which compute the rank of a matrix literal with non-symbolic entries through an Echelon.Decomposition certificate checked by the kernel.

source
def Mathlib.Tactic.Echelon.normalizeRank {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (e : Lean.Expr) (A : Q(Matrix (Fin «$m») (Fin «$n») «$α»)) (entries : Array (Array Lean.Expr)) :
Lean.MetaM Lean.Meta.Simp.Result

Rewrite Matrix.rank A to the pivot count of the Bareiss decomposition of the matrix literal A.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Mathlib.Tactic.Echelon.normRankCore :
    Lean.Meta.Simp.Simproc

    Core of the norm_rank simproc.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def norm_rank :
      Lean.Meta.Simp.Simproc

      The norm_rank simproc evaluates the rank of matrices with non-symbolic entries. Terms that it cannot evaluate are skipped, since the fallback model accepts every ring and only the evaluation can tell whether an entry is in its scope.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def evalRank :
        Lean.ParserDescr

        eval_rank evaluates the rank of matrices with non-symbolic entries.

        The element type must be a commutative domain with kernel-decidable equality. Terms skipped can be viewed by using set_option trace.Tactic.evalRank true.

        Equations
        Instances For