mathlib3
2125676c - feat(data/pfun): Product of partial functions (#15389)

Commit

3 years ago

feat(data/pfun): Product of partial functions (#15389) Define `pfun.prod : (α →. γ) → (β →. δ) → α × β →. γ × δ`.

Author

YaelDillies

Committer

b-mehta

Parents