Commit af6c796
committed
Remove discrete derivative material
It won't be used in any combinatorics course nor my PhD, hence doesn't seem like a good fit for this project. Furthermore, Mathlib recently acquired `fwdDiff`, which is a very similar definition to `discConv`, and someone provided Lean code on Zulip that proves the original theorem that motivated this file. See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Supplement.20to.20the.20fwdDiff.20theorem.20in.20mathelib.1 parent 4b9535b commit af6c796
2 files changed
+0
-122
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
3 | 3 | | |
4 | 4 | | |
5 | 5 | | |
6 | | - | |
7 | 6 | | |
8 | 7 | | |
9 | 8 | | |
| |||
This file was deleted.
0 commit comments