equivUnits

Mathlib.Algebra.AddConstMap.Equiv

URI: https://scilib.ai/kg/mathlib#AddConstEquiv.equivUnits

Lean4

/-- Group equivalence between `G ≃+c[a, a] G` and the units of `G →+c[a, a] G`. -/
@[simps!]
def equivUnits : (G ≃+c[a, a] G) ≃* (G →+c[a, a] G)ˣ
    where
  toFun := toAddConstMapHom.toHomUnits
  invFun
    u :=
    { toEquiv := Equiv.Perm.equivUnitsEnd.symm <| Units.map AddConstMap.toEnd u
      map_add_const' := u.1.2 }
  map_mul' _ _ := rfl

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

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

Разделы

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

Аффилиация

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