Def Prod.mk.injArrow

Modification history

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