mathlib3
40f582b9 - feat(data/*/nat_antidiagonal): induction lemmas about antidiagonals (#4193)

Commit
5 years ago
feat(data/*/nat_antidiagonal): induction lemmas about antidiagonals (#4193) Adds a `nat.antidiagonal_succ` lemma for `list`, `multiset`, and `finset`, useful for proving facts about power series derivatives Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Author
Parents
Loading