mem_units_of_val_mem_inv_val_mem

Mathlib.Algebra.Group.Submonoid.Units

URI: https://scilib.ai/kg/mathlib#Submonoid.mem_units_of_val_mem_inv_val_mem

← MathLib Explorer

English

If x ∈ S as an element with both x and x⁻¹ in S, then x ∈ S.units.

Русский

Если x ∈ S и x⁻¹ ∈ S как элементы, то x ∈ S.units.

LaTeX

$$x ∈ S.units$$

Lean4

@[to_additive]
theorem mem_units_of_val_mem_inv_val_mem (S : Submonoid M) {x : Mˣ} (h₁ : (x : M) ∈ S) (h₂ : ((x⁻¹ : Mˣ) : M) ∈ S) :
    x ∈ S.units :=
  ⟨h₁, h₂⟩

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

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

Разделы

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

Аффилиация

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