mem_of_mem_val_ofUnits

Mathlib.Algebra.Group.Submonoid.Units

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

← MathLib Explorer

English

From x ∈ S.ofUnits one obtains a unit in M whose value is x.

Русский

Из x ∈ S.ofUnits получают единицу в M, которая имеет значение x.

LaTeX

$$$ S.unit_of_mem_ofUnits h : M^{\times} $$$

Lean4

@[to_additive]
theorem mem_of_mem_val_ofUnits (S : Subgroup Mˣ) {y : Mˣ} (hy : (y : M) ∈ S.ofUnits) : y ∈ S :=
  match hy with
  | ⟨_, hm, he⟩ => (Units.ext he) ▸ hm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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