mathlib3
744170a9 - 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

Parents