theorem
proved
combinatoricsFamilyCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.CombinatoricsFromRS on GitHub at line 29.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
26 | permutations | combinations | partitions | paths | youngTableaux
27 deriving DecidableEq, Repr, BEq, Fintype
28
29theorem combinatoricsFamilyCount : Fintype.card CombinatoricsFamily = 5 := by decide
30
31/-- C(8,4) = 70. -/
32theorem choose84_eq_70 : Nat.choose 8 4 = 70 := by decide
33
34/-- C(8,4) = 70 > gap45 = 45. -/
35theorem choose84_gt_gap45 : Nat.choose 8 4 > 45 := by decide
36
37/-- C(8,4) = 2 × 35 = 2 × C(7,3). -/
38theorem choose84_doubled : Nat.choose 8 4 = 2 * Nat.choose 7 3 := by decide
39
40structure CombinatoricsCert where
41 five_families : Fintype.card CombinatoricsFamily = 5
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