Theorem MvPFunctor.const.get_mk

Modification history

2023-10-19 09:56
Mathlib/Data/PFunctor/Multivariate/Basic.lean
style: `CoeFun` for `PFunctor.Obj` & `MvPFunctor.Obj` (#7526)
Modified MvPFunctor.const.get_mkView on Github →
2023-09-08 21:07
Mathlib/Data/PFunctor/Multivariate/Basic.lean
chore: simplify `by rfl` (#7039)
Modified MvPFunctor.const.get_mkView on Github →
2023-02-18 19:03
Mathlib/Data/PFunctor/Multivariate/Basic.lean
feat: port Data.Pfunctor.Multivariate.Basic (#1835)
Added MvPFunctor.const.get_mkView on Github →