Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.id_def

Modification history

2020-12-10 10:51

src/logic/function/basic.lean

refactor(data/finsupp/basic): merge `finsupp.of_multiset` and `multiset.to_finsupp` (#5237) …

Added function.id_def View on Github →