of_algEquiv — Mathlib

English

If e: D ≃ₐ[K] D' is an algebra isomorphism and D is central over K, then D' is central over K.

Русский

Пусть e: D ≃ₐ[K] D' — алгебраическое изоморфизм; если D центрально относительно K, то и D' центрально относительно K.

LaTeX

$$$\\forall (e: D \\cong_{K} D'), IsCentral\\ K D'$$

Lean4

theorem of_algEquiv (e : D ≃ₐ[K] D') : IsCentral K D' where
  out x
    hx :=
    have ⟨k, hk⟩ := h.1 ((MulEquivClass.apply_mem_center_iff e.symm).mpr hx)
    ⟨k, by simpa [ofId] using congr(e $hk)⟩

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