Def PProd.mk.injArrow

Modification history

2024-08-15 12:19
Mathlib/Data/Prod/PProd.lean
chore: cleanup in Mathlib/Init/* (#15188) …
Modified PProd.mk.injArrowView on Github →
2022-10-24 02:02
Mathlib/Init/Core.lean
feat: align `init.{core, logic}` (#490) …
Added PProd.mk.injArrowView on Github →