instSubmonoidClass — Mathlib

English

The type Submonoid M naturally carries the structure of a SubmonoidClass for M, i.e., membership and multiplication are governed by the Submonoid axioms.

Русский

Тип Submonoid M естественно обладает структурой SubmonoidClass для M: членство и умножение задаются аксиомами Submonoid.

LaTeX

$$$$ \\text{Submonoid } M \\text{ is a SubmonoidClass for } M $$$$

Lean4

@[to_additive]
instance : SubmonoidClass (Submonoid M) M where
  one_mem := Submonoid.one_mem'
  mul_mem {s} := s.mul_mem'

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