theorem Prod.neq_zero_iff {α β : Type} [Zero α] [Zero β] (p : α × β) : p ≠ 0 ↔ p.1 ≠ 0 ∨ p.2 ≠ 0

@[simp]

theorem Prod.swap_eq_zero {α β : Type} [Zero α] [Zero β] (p : α × β) : p.swap = 0 ↔ p = 0

@[simp]

theorem Prod.swap_ne_zero {α β : Type} [Zero α] [Zero β] (p : α × β) : p.swap ≠ 0 ↔ p ≠ 0

def Prod.swap_emb {α β : Type} : α × β ↪ β × α

Equations

• Prod.swap_emb = { toFun := Prod.swap, inj' := ⋯ }

theorem Prod.swap_emb_coe {α β : Type} : ⇑swap_emb = swap

theorem Prod.fst_snd {α β : Type} (p : α × β) : p = (p.1, p.2)

theorem Prod.neq_iff_fst_neq_or_snd_eq {α β : Type} (p q : α × β) : p ≠ q ↔ p.1 ≠ q.1 ∨ p.2 ≠ q.2