Commit 2024-01-05 06:57 901b7832

View on Github →

feat: Zhu Shijie's identity (#9427) Cf. https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Proof.20of.20Combinatorial.20Identities/near/411120131

Estimated changes

added theorem Nat.sum_Icc_choose