Mathlib v3 is deprecated. Go to Mathlib v4

Inductive multiset.rel

Modification history

2020-11-03 17:56
src/data/multiset/basic.lean
feat(tactic/mk_iff_of_inductive_prop): mk_iff attribute (#4863) …
Modified multiset.relView on Github →
2018-05-10 15:29
data/multiset.lean
feat(data/multiset): add relator
Modified multiset.relView on Github →
2018-05-04 16:10
tests/mk_iff_of_inductive.lean
feat(tactic/mk_iff_of_inductive_prop): add tactic to represent inductives using logical connectives
Added multiset.relView on Github →