Revision #3066 → #3585 · back to history
addedCounting compositions of 1s and 2s (Fibonacci)cdf3471e4f08
modifiedSushruta's 63 combinations of tastesef5a1b8a776e
| Field | From #3066 | To #3585 |
|---|
| note | The count 2^6 − 1 = 63 nonempty subsets is a special case of `Finset.card_powerset` (verified to exist), but the specific story is not formalized. | The count 2^6 − 1 = 63 nonempty subsets is a special case of `Finset.card_powerset` (verified), but the specific story is not formalized. |
modifiedPermutation and combination formulas632571527418
| Field | From #3066 | To #3585 |
|---|
| note | The formula for combinations is `Nat.choose` and for permutations `Nat.descFactorial`; both are formalized in Mathlib. | The formula for combinations is `Nat.choose` (verified) and for permutations `Nat.descFactorial`; both are formalized in Mathlib. |
addedClassification of finite simple groups09f892a907e4
addedFinite Markov chainsfe933b7db9e7