exists_mem_ofUnits_val_eq

Mathlib.Algebra.Group.Submonoid.Units

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

English

There exists a unit y ∈ S such that y.val = x for any x ∈ S.ofUnits.

Русский

Существуют единицы y ∈ S такие, что y.val = x для любого x ∈ S.ofUnits.

LaTeX

$$$ \exists y \in S, y = x $$$

Lean4

@[to_additive]
theorem exists_mem_ofUnits_val_eq (S : Subgroup Mˣ) {x : M} (h : x ∈ S.ofUnits) : ∃ y ∈ S, y = x :=
  h

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

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

Разделы

Аффилиация

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