centerCongr — Mathlib

English

Let G and H be groups and e: G ≃* H a group isomorphism. Then the centers Z(G) and Z(H) are isomorphic via e.

Русский

Пусть G и H — группы, e: G ≃* H — изоморфизм групп. Тогда центры Z(G) и Z(H) изоморфны через e.

LaTeX

$$$Z(G) \cong Z(H)$$$

Lean4

/-- The center of isomorphic groups are isomorphic. -/
@[to_additive (attr := simps!) /-- The center of isomorphic additive groups are isomorphic. -/
    ]
def centerCongr {H} [Group H] (e : G ≃* H) : center G ≃* center H :=
  Submonoid.centerCongr e

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