toProd — Mathlib

English

The natural projection toProd: M ∗ N →* M × N satisfies (toProd) ∘ inl = inl and (toProd) ∘ inr = inr.

Русский

Естественное отображение toProd: M ∗ N →* M × N удовлетворяет (toProd) ∘ inl = inl и (toProd) ∘ inr = inr.

LaTeX

$$$\\\\mathrm{toProd} \\\\circ \\\\mathrm{inl} = \\\\mathrm{inl} \\\\_{M,N}, \\\\quad \\\\mathrm{toProd} \\\\circ \\\\mathrm{inr} = \\\\mathrm{inr} \\\\_{M,N}.$$$

Lean4

/-- The natural projection `M ∗ N →* M × N`. -/
@[to_additive toProd /-- The natural projection `AddMonoid.Coprod M N →+ M × N`. -/
    ]
def toProd : M ∗ N →* M × N :=
  lift (.inl _ _) (.inr _ _)

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