instMonoid — Mathlib

English

The dilations α →ᵈ α form a monoid under composition, with identity given by id_α and associativity of composition.

Русский

Дилатации пространства α в себя образуют моноид при композицией, единицей выступает тождественная дилатация, композиция ассоциативна.

LaTeX

$$$(\\{\\text{Dilation }\\alpha\\alpha, \\; \\circ, \\mathrm{Id}_\\alpha\\}) \\text{ образуют моноид.}$$$

Lean4

instance : Monoid (α →ᵈ α) where
  one := Dilation.id α
  mul := comp
  mul_one := comp_id
  one_mul := id_comp
  mul_assoc _ _ _ := comp_assoc _ _ _

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