mem_ofUnits_iff

Mathlib.Algebra.Group.Submonoid.Units

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

English

For S a subgroup of Units M, x ∈ S.ofUnits iff there exists a y ∈ S with y = x.

Русский

Для S, подгруппы единиц M, x ∈ S.ofUnits эквивалентно существованию y ∈ S с y = x.

LaTeX

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

Lean4

@[to_additive]
theorem mem_ofUnits_iff (S : Subgroup Mˣ) (x : M) : x ∈ S.ofUnits ↔ ∃ y ∈ S, y = x :=
  Iff.rfl

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

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

Разделы

Аффилиация

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