comp_algebraMap — Mathlib

English

For φ: A →ₐ[R] B, the RingHom underlying φ composed with the algebra map equals the algebra map after φ: (RingHom φ).comp (algebraMap) = algebraMap ∘ φ.

Русский

Для φ: A →ₐ[R] B верно: сопоставление цепочек якорных отображений согласуется: (φ).comp (algebraMap) = algebraMap ∘ φ.

LaTeX

$$$(RingHomClass.toRingHom φ).comp (algebraMap R A) = algebraMap R B$$$

Lean4

theorem comp_algebraMap : (φ : A →+* B).comp (algebraMap R A) = algebraMap R B :=
  RingHom.ext <| φ.commutes

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