LeanPool.Rupert.MatrixSimps

Imported Lean Pool material for LeanPool.Rupert.MatrixSimps.

def matrixReduceNatAdd : Lean.Meta.Simp.DSimproc

Reduce natural additions in concrete matrix expressions.

Equations

• matrixReduceNatAdd = Nat.reduceAdd

def matrixNormalizeFin : Lean.Meta.Simp.DSimproc

Normalize finite indices in concrete matrix expressions.

Equations

• matrixNormalizeFin = Fin.isValue