units_ofUnits_eq

Mathlib.Algebra.Group.Submonoid.Units

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

← MathLib Explorer

English

Equality of units under the ofUnits map: Subgroup.units_ofUnits_eq.

Русский

Равенство единиц под маппинга ofUnits: Subgroup.units_ofUnits_eq.

LaTeX

$$S.units_ofUnits_eq$$

Lean4

@[to_additive (attr := simp)]
theorem units_ofUnits_eq (S : Subgroup Mˣ) : S.ofUnits.units = S :=
  Subgroup.ext (fun _ => ⟨fun ⟨⟨_, hm, he⟩, _⟩ => (Units.ext he) ▸ hm, fun hm => ⟨⟨_, hm, rfl⟩, _, S.inv_mem hm, rfl⟩⟩)

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

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

Разделы

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

Аффилиация

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