commSemigroup — Mathlib

English

There is a transported commutative semigroup structure on α from β along e, with the same compatibility condition as for a semigroup.

Русский

Существует перенесённая через e коммутативная полугруппа на α, полученная из β; совместимость аналогична случаю полугруппы.

LaTeX

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

Lean4

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

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