Commit 2023-02-20 12:02 8c1e4fb3

View on Github →

feat: port Data.Pfunctor.Multivariate.M (#2362)

Estimated changes

Modified Mathlib.lean

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

added inductive MvPFunctor.M.Path

added theorem MvPFunctor.M.bisim'

added theorem MvPFunctor.M.bisim

added theorem MvPFunctor.M.bisim_lemma

added theorem MvPFunctor.M.bisim₀

added def MvPFunctor.M.corec'

added def MvPFunctor.M.corec

added def MvPFunctor.M.corecContents

added def MvPFunctor.M.corecShape

added def MvPFunctor.M.dest'

added theorem MvPFunctor.M.dest'_eq_dest'

added def MvPFunctor.M.dest

added theorem MvPFunctor.M.dest_corec'

added theorem MvPFunctor.M.dest_corec

added theorem MvPFunctor.M.dest_eq_dest'

added theorem MvPFunctor.M.dest_map

added theorem MvPFunctor.M.map_dest

added def MvPFunctor.M.mk

added def MvPFunctor.M.pathDestLeft

added def MvPFunctor.M.pathDestRight

added def MvPFunctor.M

added def MvPFunctor.castDropB

added def MvPFunctor.castLastB

added def MvPFunctor.mp