inv_mem_iff

Mathlib.Algebra.Group.Subgroup.Defs

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

English

x^{-1} ∈ H if and only if x ∈ H.

Русский

x^{-1} ∈ H ⇔ x ∈ H.

LaTeX

$$$x^{-1} \\in H \\iff x \\in H$$$

Lean4

@[to_additive]
protected theorem inv_mem_iff {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
  inv_mem_iff

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

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

Разделы

Аффилиация

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