norm_det simproc and eval_det tactic

This module defines the norm_det simproc and the eval_det tactic for normalizing determinants of matrix literals over a commutative ring.

def norm_det : Lean.Meta.Simp.Simproc

The norm_det simproc normalizes determinants of matrices written using !![...] notation over a commutative ring.

Equations

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

def evalDet : Lean.ParserDescr

eval_det normalizes determinants of matrices written using !![...] notation over a commutative ring.

Examples:

example : Matrix.det (R := ℤ) !![1, 2; 3, 4] = -2 := by
  eval_det

example {R : Type*} [CommRing R] (a b c d : R) :
    Matrix.det !![a, b; c, d] = a * d - b * c := by
  eval_det
  ring

Equations

• evalDet = Lean.ParserDescr.node `evalDet 1024 (Lean.ParserDescr.nonReservedSymbol "eval_det" false)