algEquiv_apply_map — Mathlib

English

Composition of adjacent root isomorphisms is associative: (h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h''.

Русский

Составление последовательных изоморфизмов по присоединению корня даёт ассоциативность: (h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h''.

LaTeX

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

Lean4

@[simp]
theorem algEquiv_apply_map (z : R[X]) : h.algEquiv h' (h.map z) = h'.map z := by rw [← h.algEquiv_map h'];
  simp [-algEquiv_map]

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