instMonoid — Mathlib

English

CircleDeg1Lift carries a monoid structure with multiplication given by composition and identity given by the identity lift.

Русский

CircleDeg1Lift образует моноид: умножение задаётся как композиция отображений, единица — это тождественное отображение.

LaTeX

$$$\\text{CircleDeg1Lift}$ образует моноид под операцией $(f*g)(x)=f(g(x))$ и единицей $1(x)=x$.$$

Lean4

instance : Monoid CircleDeg1Lift
    where
  mul f
    g :=
    { toOrderHom := f.1.comp g.1
      map_add_one' := fun x => by simp [map_add_one] }
  one := ⟨.id, fun _ => rfl⟩
  mul_one _ := rfl
  one_mul _ := rfl
  mul_assoc _ _ _ := DFunLike.coe_injective rfl

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