Theorem Choose.choose_modEq_choose_mod_mul_choose_div

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_mod_mul_choose_divView on Github →