def definition def or abbrev

`linearAlgebraCert`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  42def linearAlgebraCert : LinearAlgebraCert where
  43  five_ops := linearAlgebraOpCount

Definition body.

  44  dimension_3 := rsDimension_eq_3
  45  f2cube_8 := f2CubeSize_eq_8
  46
  47end IndisputableMonolith.Mathematics.LinearAlgebraFromRS

Lean names referenced from this declaration's body.

f2CubeSize_eq_8 in IndisputableMonolith.Mathematics.LinearAlgebraFromRS decl_use
LinearAlgebraCert in IndisputableMonolith.Mathematics.LinearAlgebraFromRS decl_use
linearAlgebraOpCount in IndisputableMonolith.Mathematics.LinearAlgebraFromRS decl_use
rsDimension_eq_3 in IndisputableMonolith.Mathematics.LinearAlgebraFromRS decl_use