mathlib documentation

data.pprod

Extra facts about pprod

@[simp]
theorem pprod.mk.eta {α : Sort u_1} {β : Sort u_2} {p : pprod α β} :
p.fst, p.snd = p