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 (e A : Lean.Expr) (m n : ℕ) (R : Lean.Expr) (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.

      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