Commit 2023-03-12 11:16 e03f4dcc

View on Github →

feat: port Data.Nat.Choose.Cast (#2821)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Choose/Cast.lean

added theorem Nat.cast_add_choose

added theorem Nat.cast_choose

added theorem Nat.cast_choose_eq_pochhammer_div

added theorem Nat.cast_choose_two