Documentation

Mathlib.Init.Data.Prod

alignments from lean 3 init.data.prod #

@[simp]
theorem Prod.mk.eta {α : Type u} {β : Type v} {p : α × β} :
(p.fst, p.snd) = p