mathlib3 documentation

core / init.data.prod

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