instMonoid — Mathlib

English

There is a Monoid structure on the set of affine endomorphisms P1 →ᵃ[k] P1 with one = id and multiplication = comp.

Русский

Существует структура моноида на множестве аффинных эндоморфизмов P1 →ᵃ[k] P1, где единица — это id, а умножение — композиция.

LaTeX

$$$\\text{Monoid}(P_1 \\to\\!^a_k P_1)$ with one = id, mul = comp, one_mul = id_comp, mul_one = comp_id, and assoc = comp_assoc.$$

Lean4

instance : Monoid (P1 →ᵃ[k] P1) where
  one := id k P1
  mul := comp
  one_mul := id_comp
  mul_one := comp_id
  mul_assoc := comp_assoc

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