unit_eq_unit_of_mem_ofUnits

Mathlib.Algebra.Group.Submonoid.Units

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

← MathLib Explorer

English

If h₁ is a unit and h₂ ∈ S.ofUnits, then h₁.unit equals S.unit_of_mem_ofUnits h₂.

Русский

Если h₁ — единица, а h₂ ∈ S.ofUnits, то h₁.unit = S.unit_of_mem_ofUnits h₂.

LaTeX

$$$ h_1.un = S.unit_of_mem_ofUnits h_2 $$$

Lean4

@[to_additive]
theorem unit_eq_unit_of_mem_ofUnits (S : Subgroup Mˣ) {x : M} (h₁ : IsUnit x) (h₂ : x ∈ S.ofUnits) :
    h₁.unit = S.unit_of_mem_ofUnits h₂ :=
  Units.ext rfl

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

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

Разделы

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

Аффилиация

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