algEquiv_algEquiv — Mathlib

English

For IsAdjoinRoot S f, IsAdjoinRoot T f, and U f, the map of algEquivs is compatible: (h.AlgEquiv h') acts compatibly with triple composition.

Русский

Для тройного набора IsAdjoinRoot совместимость: сравнительная совместимость алгеброизоморфизмов.

LaTeX

$$$(h'.algEquiv h'') (h.algEquiv h' x) = h.algEquiv h'' x$ for all x$$

Lean4

@[simp]
theorem algEquiv_algEquiv {U : Type*} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) (x) :
    (h'.algEquiv h'') (h.algEquiv h' x) = h.algEquiv h'' x := by simp [algEquiv_def]

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