inv_val_mem_of_mem_units

Mathlib.Algebra.Group.Submonoid.Units

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

English

If x ∈ S.units, then x⁻¹ ∈ S.

Русский

Если x ∈ S.units, то x⁻¹ ∈ S.

LaTeX

$$x^{-1} ∈ S$$

Lean4

@[to_additive]
theorem inv_val_mem_of_mem_units (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) : ((x⁻¹ : Mˣ) : M) ∈ S :=
  h.2

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

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

Разделы

Аффилиация

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