pith. machine review for the scientific record. sign in
structure definition def or abbrev

CountLawCert

show as:
view Lean formalization →

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)

 177structure CountLawCert where
 178  card_law :
 179    ∀ {D : ℕ} {Family : Type} [Fintype Family]
 180      {encoding : Family → F2Power D},
 181      CountLaw D Family encoding → Fintype.card Family = 2 ^ D - 1
 182  no_extra :
 183    ∀ {D : ℕ} {Family : Type} [Fintype Family]
 184      {encoding : Family → F2Power D},
 185      CountLaw D Family encoding →
 186        ∀ v : F2Power D, v ≠ 0 → ∃ x : Family, encoding x = v
 187  booker_instance :
 188    CountLaw 3 BookerPlotFamily plotEncoding
 189  booker_card_via_law :
 190    Fintype.card BookerPlotFamily = 7
 191
 192/-- The master certificate is inhabited. -/

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.