centerCongr

Mathlib.GroupTheory.Submonoid.Center

URI: https://scilib.ai/kg/mathlib#Subsemigroup.centerCongr

Lean4

/-- The center of isomorphic magmas are isomorphic. -/
@[to_additive (attr := simps) /-- The center of isomorphic additive magmas are isomorphic. -/
    ]
def centerCongr [Mul M] [Mul N] (e : M ≃* N) : center M ≃* center N
    where
  toFun r := ⟨e r, MulEquivClass.apply_mem_center e r.2⟩
  invFun s := ⟨e.symm s, MulEquivClass.apply_mem_center e.symm s.2⟩
  left_inv _ := Subtype.ext (e.left_inv _)
  right_inv _ := Subtype.ext (e.right_inv _)
  map_mul' _ _ := Subtype.ext (map_mul ..)

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

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

Разделы

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

Аффилиация

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