structure definition def or abbrev

`ClassicalCode`

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

formal statement (Lean)

 112structure ClassicalCode where
 113  n : ℕ  -- Block length
 114  k : ℕ  -- Message length
 115  d : ℕ  -- Minimum distance
 116  k_le_n : k ≤ n
 117  d_pos : d > 0
 118
 119/-- The 3-qubit repetition code.
 120
 121    |0⟩ → |000⟩
 122    |1⟩ → |111⟩
 123
 124    Corrects single bit-flip errors. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

CSSCode in IndisputableMonolith.Information.QuantumErrorCorrection decl_use
repetitionCode3 in IndisputableMonolith.Information.QuantumErrorCorrection decl_use

depends on (1)

Lean names referenced from this declaration's body.

Block in IndisputableMonolith.Chemistry.PeriodicTable decl_use