Theorem Choose.choose_modEq_choose_mul_prod_range_choose

Modification history

2024-07-23 14:14
Mathlib/Data/Nat/Choose/Lucas.lean
feat(Data/Nat/Choose): Lucas' theorem (#8612) …
Added Choose.choose_modEq_choose_mul_prod_range_chooseView on Github →