Commit 2023-02-18 19:03 f14b8b1c

View on Github →

feat: port Data.Pfunctor.Multivariate.Basic (#1835)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/PFunctor/Multivariate/Basic.lean

added def MvPFunctor.Obj

added def MvPFunctor.appendContents

added def MvPFunctor.comp.get

added theorem MvPFunctor.comp.get_map

added theorem MvPFunctor.comp.get_mk

added def MvPFunctor.comp.mk

added theorem MvPFunctor.comp.mk_get

added def MvPFunctor.comp

added theorem MvPFunctor.comp_map

added def MvPFunctor.const.get

added theorem MvPFunctor.const.get_map

added theorem MvPFunctor.const.get_mk

added def MvPFunctor.const.mk

added theorem MvPFunctor.const.mk_get

added def MvPFunctor.const

added def MvPFunctor.drop

added theorem MvPFunctor.id_map

added def MvPFunctor.last

added theorem MvPFunctor.liftP_iff'

added theorem MvPFunctor.liftP_iff

added theorem MvPFunctor.liftR_iff

added def MvPFunctor.map

added theorem MvPFunctor.map_eq

added theorem MvPFunctor.supp_eq

added structure MvPFunctor