submonoid — Mathlib

English

The units of a monoid M form a submonoid of M.

Русский

Единицы моноида M образуют подмоном M.

LaTeX

$$IsUnit.submonoid M$$

Lean4

/-- The submonoid consisting of the units of a monoid -/
@[to_additive /-- The additive submonoid consisting of the additive units of an additive monoid -/
    ]
def submonoid (M : Type*) [Monoid M] : Submonoid M
    where
  carrier := setOf IsUnit
  one_mem' := by simp only [isUnit_one, Set.mem_setOf_eq]
  mul_mem' := by
    intro a b ha hb
    rw [Set.mem_setOf_eq] at *
    exact IsUnit.mul ha hb

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