algEquiv_ofAlgEquiv — Mathlib

English

Converse to the previous transfer: given h and h', and e: T ≃ₐ[R] U, h.algEquiv (h'.ofAlgEquiv e) equals (h.algEquiv h').trans e.

Русский

Обратное преобразование: дадим e, получаем равенство изоморфизмов.

LaTeX

$$$h.algEquiv (h'.ofAlgEquiv e) = (h.algEquiv h').trans e$$$

Lean4

@[simp]
theorem algEquiv_ofAlgEquiv {U : Type*} [Ring U] [Algebra R U] (e : T ≃ₐ[R] U) :
    h.algEquiv (h'.ofAlgEquiv e) = (h.algEquiv h').trans e :=
  by
  ext a
  simp [algEquiv_def, AlgEquiv.trans_apply, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply]

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