instMulMemClass

Mathlib.Algebra.Group.Subsemigroup.Defs

URI: https://scilib.ai/kg/mathlib#Subsemigroup.instMulMemClass

English

There is a canonical instance making Subsemigroup a MulMemClass, i.e., closure under multiplication respects membership: if x,y ∈ S then x*y ∈ S.

Русский

Существует канонический экземпляр, делающий Subsemigroup MulMemClass: если x,y ∈ S, то x*y ∈ S.

LaTeX

$$Subsemigroup.instMulMemClass$$

Lean4

@[to_additive]
instance : MulMemClass (Subsemigroup M) M where mul_mem := fun {_ _ _} => Subsemigroup.mul_mem' _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru