toAddSubmonoid'

Mathlib.Algebra.Group.Submonoid.Operations

URI: https://scilib.ai/kg/mathlib#Submonoid.toAddSubmonoid'

← MathLib Explorer

English

For S : ι → Submonoid M, (iInf S).op = ⨅ i, (S i).op.

Русский

Для S : ι → подмонад M, (iInf S).op = ⨅ i, (S i).op.

LaTeX

$$$ (\iInf S)^{\mathrm{op}} = \big\wedge_{i} (S(i)).op $$$

Lean4

/-- Submonoids of a monoid `Multiplicative A` are isomorphic to additive submonoids of `A`. -/
abbrev toAddSubmonoid' : Submonoid (Multiplicative A) ≃o AddSubmonoid A :=
  AddSubmonoid.toSubmonoid.symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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