isGroupoidProd — Mathlib

English

If α and β are groupoids, then their product α × β is a groupoid.

Русский

Если обе категории являются групоидами, их произведение α × β является групоидом.

LaTeX

$$$\mathrm{IsGroupoid}(\alpha \times \beta)$$$

Lean4

instance isGroupoidProd {α : Type u} {β : Type u₂} [Category.{v} α] [Category.{v₂} β] [IsGroupoid α] [IsGroupoid β] :
    IsGroupoid (α × β) where all_isIso f := (isIso_prod_iff (f := f)).mpr ⟨inferInstance, inferInstance⟩

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