`combinatoricsCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Mathematics.CombinatoricsFromRS
domain: Mathematics
line: 45 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Mathematics.CombinatoricsFromRS on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  42  choose84 : Nat.choose 8 4 = 70
  43  choose84_gt : Nat.choose 8 4 > 45
  44
  45def combinatoricsCert : CombinatoricsCert where
  46  five_families := combinatoricsFamilyCount
  47  choose84 := choose84_eq_70
  48  choose84_gt := choose84_gt_gap45
  49
  50end IndisputableMonolith.Mathematics.CombinatoricsFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.