Def MvPFunctor.objAppend1

Modification history

2024-05-07 01:05
Mathlib/Data/PFunctor/Multivariate/W.lean
refactor: replace `@[reducible]` with `abbrev` (#12614) …
Deleted MvPFunctor.objAppend1View on Github →
2023-10-17 09:07
Mathlib/Data/PFunctor/Multivariate/W.lean
chore: remove many `Type _` before the colon (#7718) …
Modified MvPFunctor.objAppend1View on Github →
2023-02-20 13:00
Mathlib/Data/PFunctor/Multivariate/W.lean
feat: Port Data.PFunctor.Multivariate.W (#2233)
Added MvPFunctor.objAppend1View on Github →