def definition def or abbrev

`countLawCert`

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

formal statement (Lean)

 193def countLawCert : CountLawCert where
 194  card_law := countLaw_implies_card

proof body

Definition body.

 195  no_extra := countLaw_implies_no_extra
 196  booker_instance := bookerCountLaw
 197  booker_card_via_law := booker_count_via_law
 198
 199end
 200
 201end TwoToTheDMinusOne
 202end Patterns
 203end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.

bookerCountLaw in IndisputableMonolith.Patterns.TwoToTheDMinusOne decl_use
booker_count_via_law in IndisputableMonolith.Patterns.TwoToTheDMinusOne decl_use
CountLawCert in IndisputableMonolith.Patterns.TwoToTheDMinusOne decl_use
countLaw_implies_card in IndisputableMonolith.Patterns.TwoToTheDMinusOne decl_use
countLaw_implies_no_extra in IndisputableMonolith.Patterns.TwoToTheDMinusOne decl_use