instMonoid — Mathlib

English

The collection of all affine isometries P → P forms a monoid under composition, with the identity map as the unit and composition as the binary operation.

Русский

Множество всех аффинных изометрий P → P образует моноид относительно композиции, единицей является тождественное отображение, умножение задаётся посредством композиции.

LaTeX

$$$$ \text{AffineIsometry}(P,P) \text{ forms a monoid under composition: } 1 = \mathrm{id},\; (f\cdot g)(x) = f(g(x)). $$$$

Lean4

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

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