Commit 2023-06-01 23:29 2b30bc37
View on Github →feat: forward-port 2 lemmas from mathlib3 (#4542)
These lemmas are in the analysis.calculus.cont_diff file with a
porting comment saying to move them to Data.Nat.Choose.Sum. I moved
them, golfed, and added multiplicative versions.