theorem
other
other
qecCodeFamilyCount
No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
29theorem qecCodeFamilyCount : Fintype.card QECCodeFamily = 5 := by decide
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
qecThresholdCert
in IndisputableMonolith.Information.QECThresholdFromPhiLadder
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
QECCodeFamily
in IndisputableMonolith.Information.QECThresholdFromPhiLadder
decl_use