theorem
proved
f2CubeSize_eq_8
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.LinearAlgebraFromRS on GitHub at line 35.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
32def f2CubeSize : ℕ := 2 ^ rsDimension
33
34theorem rsDimension_eq_3 : rsDimension = 3 := rfl
35theorem f2CubeSize_eq_8 : f2CubeSize = 8 := by decide
36
37structure LinearAlgebraCert where
38 five_ops : Fintype.card LinearAlgebraOp = 5
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