mem_toSubmonoid

Mathlib.Algebra.Group.Subgroup.Defs

URI: https://scilib.ai/kg/mathlib#Subgroup.mem_toSubmonoid

English

For any x in G, x belongs to K.toSubmonoid if and only if x belongs to K.

Русский

Для любого x из G верно: x принадлежит K.toSubmonoid тогда и только тогда, когда x принадлежит K.

LaTeX

$$$x \\in K^{\\text{submonoid}} \\iff x \\in K$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_toSubmonoid (K : Subgroup G) (x : G) : x ∈ K.toSubmonoid ↔ x ∈ K :=
  Iff.rfl

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

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

Разделы

Аффилиация

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