semigroup — Mathlib

English

There is a canonical Semigroup structure on α transported from β along e, i.e., multiplication on α is defined so that e(xy) = e x · e y.

Русский

Существует каноническая полугруппа на α, полученная по переносу из β через e; умножение на α таково, чтобы e(xy) = e x · e y.

LaTeX

$$$$e(xy) = e(x)\cdot e(y).$$$$

Lean4

/-- Transfer `Semigroup` across an `Equiv` -/
@[to_additive /-- Transfer `add_semigroup` across an `Equiv` -/
    ]
protected abbrev semigroup [Semigroup β] : Semigroup α :=
  by
  let mul := e.mul
  apply e.injective.semigroup _; intros; exact e.apply_symm_apply _

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