mapAlgEquiv_comp — Mathlib

English

Composition of polynomial-algebra maps corresponds to composing their algebra isomorphisms: mapAlgEquiv f followed by mapAlgEquiv g equals mapAlgEquiv (f trans g).

Русский

Составление отображений многочленов соответствует композиции соответствующих алгебраических эквивалентов: mapAlgEquiv f, затем mapAlgEquiv g, даёт mapAlgEquiv (f.trans g).

LaTeX

$$$$ (\mathrm{Polynomial.mapAlgEquiv}(f)).trans (\mathrm{Polynomial.mapAlgEquiv}(g)) = \mathrm{Polynomial.mapAlgEquiv}(f \textrm{.trans } g).$$$$

Lean4

@[simp]
theorem mapAlgEquiv_comp (C : Type*) [Semiring C] [Algebra R C] (f : A ≃ₐ[R] B) (g : B ≃ₐ[R] C) :
    (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g) :=
  by
  ext
  simp

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