inv_mem_units_iff

Mathlib.Algebra.Group.Submonoid.Units

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

English

For a submonoid S, x^{-1} ∈ S.units if and only if x ∈ S.units.

Русский

Для подмодуля S: x^{-1} ∈ S.units тогда и только тогда, когда x ∈ S.units.

LaTeX

$$$ x^{-1} \in S.units \iff x \in S.units $$$

Lean4

@[to_additive]
theorem inv_mem_units_iff (S : Submonoid M) {x : Mˣ} : x⁻¹ ∈ S.units ↔ x ∈ S.units :=
  inv_mem_iff

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

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

Разделы

Аффилиация

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