centerCongr — Mathlib

English

The center is preserved under ring isomorphisms: given a ring isomorphism e : R ≃+* S, there is an isomorphism between centers.

Русский

Центр сохраняется при изоморфизмах колец: есть изоморфизм между центрами

LaTeX

$$center R ≃+* center S$$

Lean4

/-- The center of isomorphic (not necessarily associative) rings are isomorphic. -/
@[simps!]
def centerCongr (e : R ≃+* S) : center R ≃+* center S :=
  NonUnitalSubsemiring.centerCongr e

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