mem_ofUnits

Mathlib.Algebra.Group.Submonoid.Units

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

English

For a subgroup S of Units M and x ∈ M, x ∈ S.ofUnits iff ∃ y ∈ S, y = x.

Русский

Для подгруппы S единиц M, x ∈ S.ofUnits тогда и только тогда, когда ∃ y ∈ S, y = x.

LaTeX

$$$ x \in S.ofUnits \iff \exists y \in S, y = x $$$

Lean4

@[to_additive]
theorem mem_ofUnits (S : Subgroup Mˣ) {x : M} {y : Mˣ} (h₁ : y ∈ S) (h₂ : y = x) : x ∈ S.ofUnits :=
  ⟨_, h₁, h₂⟩

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

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

Разделы

Аффилиация

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