Theorem Choose.choose_modEq_prod_range_choose_nat

Modification history

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