coe_bot — Mathlib

English

In any multiplicative monoid M, the bottom submonoid has as its underlying set the singleton {1}; only the identity element is included.

Русский

В любом моноиде M нижний субмонод имеет в качестве множества-основы лишь концевое множество {1}; присутствует только тождественный элемент.

LaTeX

$$$((\bot : \mathrm{Submonoid} M) : \mathrm{Set} M) = \{ 1 \}$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_bot : ((⊥ : Submonoid M) : Set M) = { 1 } :=
  rfl

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