Issues

• Updates available but manual intervention required

  auto-update-lean-fail
  wurtylex/LeanECC#70 · Filter by author github-actions opened on Sep 7, 2026

• [GVB] [Lemma] Covering

  wurtylex/LeanECC#37 · Filter by author wurtylex opened on Jun 13, 2026
  

• [GVB] Gilbert-Varshamov Bound for General Codes

  wurtylex/LeanECC#35 · Filter by author wurtylex opened on Jun 13, 2026

• [GVB] Gilbert-Varshamov Bound for Linear Code

  wurtylex/LeanECC#34 · Filter by author wurtylex opened on Jun 13, 2026

• [Lemma] 2.3.7 d = size of smallest subset of H that are LD

  wurtylex/LeanECC#16 · Filter by author wurtylex opened on Jun 5, 2026

• [Lemma] 2.3.6 d = min wt(c)

  wurtylex/LeanECC#15 · Filter by author wurtylex opened on Jun 5, 2026
  

• [Lemma] 1.5.3 C(X) + C(Y) = C(X+Y)

  wurtylex/LeanECC#14 · Filter by author wurtylex opened on Jun 5, 2026

• [Lemma] Linear Code Def by Subspace = Linear Code Def by Parity Check Matrix

  wurtylex/LeanECC#13 · Filter by author wurtylex opened on Jun 5, 2026
  

• [Lemma] Linear Code Def by Subspace = Linear Code Def by Generator Matrix

  wurtylex/LeanECC#12 · Filter by author wurtylex opened on Jun 5, 2026
  

• [Definition] Binary Linear Codes

  wurtylex/LeanECC#10 · Filter by author wurtylex opened on Jun 5, 2026