mathlib3 documentation

core / init.data.prod

@[simp]
theorem prod.mk.eta {α : Type u} {β : Type v} {p : α × β} :
(p.fst, p.snd) = p
@[protected, instance]
def prod.inhabited {α : Type u} {β : Type v} [inhabited α] [inhabited β] :
inhabited × β)
Equations
@[protected, instance]
def prod.decidable_eq {α : Type u} {β : Type v} [h₁ : decidable_eq α] [h₂ : decidable_eq β] :
Equations
def prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ α₂) (g : β₁ β₂) (x : α₁ × β₁) :
α₂ × β₂
Equations