punitProd — Mathlib

English

PUnit acts as a left identity for type products up to equivalence: PUnit × α ≃ α.

Русский

PUnit служит левым тождеством для декартова произведения типов: PUnit × α ≃ α.

LaTeX

$$$$ \\mathrm{PUnit} \\times \\alpha \\simeq \\alpha. $$$$

Lean4

/-- `PUnit` is a left identity for type product up to an equivalence. -/
@[simps! (attr := grind =)]
def punitProd (α) : PUnit × α ≃ α :=
  calc
    PUnit × α ≃ α × PUnit := prodComm _ _
    _ ≃ α := prodPUnit _

Похожие утверждения