algEquiv_trans — Mathlib

English

Another associativity property of the algebra isomorphisms; transitivity yields the same overall isomorphism.

Русский

Другая ассоциативность изоморфизмов; переход через цепочку даёт тот же итоговый изоморфизм.

LaTeX

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

Lean4

@[simp]
theorem algEquiv_trans {U : Type*} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) :
    (h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h'' := by ext; simp

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