module module

`IndisputableMonolith.Patterns.TwoToTheDMinusOne`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Aesthetics.NarrativeGeodesic module_import
IndisputableMonolith.Algebra.F2Power module_import

declarations in this module (9)

structure CountLaw L75
theorem countLaw_implies_card L89
theorem countLaw_implies_no_extra L113
theorem bookerCountLaw L123
theorem booker_count_via_law L130
def OpponentColorCountLaw L152
def MassiveBosonCountLaw L161
structure CountLawCert L177
def countLawCert L193