algebraMap_apply — Mathlib

English

The application of algebraMap in a tower equals the application through the composed map.

Русский

Применение algebraMap в башне равно применению через композицию отображений.

LaTeX

$$$\text{algebraMap}_R^A(x) = \text{algebraMap}_S^A(\text{algebraMap}_R^S(x))$$$

Lean4

theorem algebraMap_apply (x : R) : algebraMap R A x = algebraMap S A (algebraMap R S x) := by
  rw [algebraMap_eq R S A, RingHom.comp_apply]

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