instRightCancelSemigroup — Mathlib

English

Let M be a right-cancellative semigroup. Then Germ_l M (the germ construction along a filter l) inherits a right-cancellative semigroup structure from M, with multiplication induced by the germ operation.

Русский

Пусть M является правой отменяемой полугруппой. Тогда конструкция Germ_l M (гермы вдоль фильтра l) наследует структуру правой отменяемой полугруппы от M, с умножением, индуцированным грем-операцией.

LaTeX

$$$\\text{RightCancelSemigroup}(M) \\Rightarrow \\text{RightCancelSemigroup}(\\mathrm{Germ}_l M).$$$

Lean4

@[to_additive]
instance instRightCancelSemigroup [RightCancelSemigroup M] : RightCancelSemigroup (Germ l M) where
  mul_right_cancel _ _ _ := mul_right_cancel

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