isoCoprod_inv — Mathlib

English

The inverse of biprod.isoCoprod is the coprod description with biprod.inl and biprod.inr.

Русский

Обратный элемент biprod.isoCoprod равен coprod.desc biprod.inl biprod.inr.

LaTeX

$$$ (\biprod.isoCoprod X Y).inv = \operatorname{coprod.desc}(\biprod.inl, \biprod.inr) $$$

Lean4

@[simp]
theorem isoCoprod_inv {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.isoCoprod X Y).inv = coprod.desc biprod.inl biprod.inr := by ext <;> simp [biprod.isoCoprod]

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