aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/binomial.v
AgeCommit message (Expand)Author
2020-11-20Tuning simplifications using Arguments simpl nomatchCyril Cohen
2020-11-13Rename `eq_sorted` lemmas to `sorted_eq` and generalize `sort_le_id`Kazuhiko Sakaguchi
2020-09-29rename mem_imset to imset_f (with deprecation)Christian Doczkal
2020-05-16A few more revisionsKazuhiko Sakaguchi
2020-05-13Revise proofs in ssreflect/*.vKazuhiko Sakaguchi
2020-04-08fix typos in documentation: formulaeAntonio Nikishaev
2020-04-08fix typos in documentation: textAntonio Nikishaev
2019-12-28Refactoring and linting especially polydivKazuhiko Sakaguchi
2019-11-27Explicit `bigop` enumeration handlingGeorges Gonthier
2019-11-22New generalised induction idiom (#434)Georges Gonthier
2019-09-30ffact as a product similar to fact_prod (#374)Laurent Théry
2019-09-16fermat little theoremthery
2019-05-08suppress use of `Arith` hintsSora Chen
2019-04-26Cleaning Require and Require ImportsCyril Cohen
2019-04-01Making {fun ...} structural and extending it to dependent functionsGeorges Gonthier
2019-03-24Compat of sumn with bigop and renaming dep to cond when appropriateCyril Cohen
2018-02-06running semi-automated linting on the whole libraryCyril Cohen
2018-02-05tide up proof of card_inj_ffunsEnrico Tassi
2016-11-07update copyright bannerAssia Mahboubi
2016-09-16Refactoring of binonialthery
2015-11-05merge basic/ into ssreflect/Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:02:27 +0000