The norm_matmul simproc

norm_matmul rewrites a product of matrix literals to the literal of the product, with the entries normalised by norm_num if possible.

Implementation notes

The product is rewritten on the row lists of the factors, and the equation between the !![…] literals follows from the one between their ofLists forms by a single definitional hint.

Note that there are simp lemmas rewriting a product of vecCons, which compete with this simproc due to how !![] is currently elaborated, so the simproc should be used by simp only.

def Mathlib.Tactic.Matrix.normMatMulCore : Lean.Meta.Simp.Simproc

Core of the norm_matmul simproc.

Equations

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

def norm_matmul : Lean.Meta.Simp.Simproc

Rewrite a product of matrix literals to the literal of the product, with the entries normalised by norm_num if possible.

Equations

• norm_matmul = Mathlib.Tactic.Matrix.normMatMulCore