val_mem_of_mem_units

Mathlib.Algebra.Group.Submonoid.Units

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

English

If x ∈ S.units, then the underlying value x ∈ S.

Русский

Если x ∈ S.units, тогда x ∈ S.

LaTeX

$$x ∈ S.units → x ∈ S$$

Lean4

@[to_additive]
theorem val_mem_of_mem_units (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) : (x : M) ∈ S :=
  h.1

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

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

Разделы

Аффилиация

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