mathlib
1ef04bde - feat(data/finsupp): prove `f.curry x y = f (x, y)` (#7475)

Commit

4 years ago

feat(data/finsupp): prove `f.curry x y = f (x, y)` (#7475) This was surprisingly hard to prove actually! To be used in the `bundled-basis` refactor

Author

Vierkantor

Parents