centerToMulOpposite — Mathlib

English

For any group G, the center of G is isomorphic to the center of its opposite group G^{op}.

Русский

Для любой группы G центр группы G изоморфен центру противоположной группы G^{op}.

LaTeX

$$$Z(G) \cong Z(G^{\mathrm{op}})$$$

Lean4

/-- The center of a group is isomorphic to the center of its opposite. -/
@[to_additive (attr := simps!) /-- The center of an additive group is isomorphic to the center of its opposite. -/
    ]
def centerToMulOpposite : center G ≃* center Gᵐᵒᵖ :=
  Submonoid.centerToMulOpposite

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