monMonoid — Mathlib

English

A canonical Monoid structure on any type A equipped with a MonObj structure is given by η[A] and μ[A].

Русский

Каноническая моноидальная структура на типе A обеспечивается η[A] и μ[A].

LaTeX

$$(A) → [MonObj A] → Monoid A$$

Lean4

instance monMonoid (A : Type u) [MonObj A] : Monoid A
    where
  one := η[A] PUnit.unit
  mul x y := μ[A] (x, y)
  one_mul x := by convert congr_fun (one_mul A) (PUnit.unit, x)
  mul_one x := by convert congr_fun (mul_one A) (x, PUnit.unit)
  mul_assoc x y z := by convert congr_fun (mul_assoc A) ((x, y), z)

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