Theorem Multiset.lift_coe

Modification history

2025-02-25 17:02
Mathlib/Data/Multiset/Basic.lean
chore(Data/Multiset): split `Multiset/Basic.lean` into many files (#22126) …
Modified Multiset.lift_coeView on Github →
2024-06-29 09:06
Mathlib/Data/Multiset/Basic.lean
chore: move `Multiset.lift_coe` (#14252) …
Modified Multiset.lift_coeView on Github →
2023-08-10 19:52
Mathlib/Data/Multiset/Functor.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified Multiset.lift_coeView on Github →
2023-01-31 17:29
Mathlib/Data/Multiset/Functor.lean
feat: Port data.multiset.functor (#1790)
Added Multiset.lift_coeView on Github →