pith. machine review for the scientific record. sign in
def

linearAlgebraCert

definition
show as:
view math explainer →
module
IndisputableMonolith.Mathematics.LinearAlgebraFromRS
domain
Mathematics
line
42 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Mathematics.LinearAlgebraFromRS on GitHub at line 42.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  39  dimension_3 : rsDimension = 3
  40  f2cube_8 : f2CubeSize = 8
  41
  42def linearAlgebraCert : LinearAlgebraCert where
  43  five_ops := linearAlgebraOpCount
  44  dimension_3 := rsDimension_eq_3
  45  f2cube_8 := f2CubeSize_eq_8
  46
  47end IndisputableMonolith.Mathematics.LinearAlgebraFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.