comp_apply — Mathlib

English

For ring homomorphisms σ12: R1 → R2, σ23: R2 → R3, and σ13: R1 → R3 satisfying the triple condition, one has σ23(σ12(x)) = σ13(x) for all x ∈ R1.

Русский

Для кольцевых гомоморфизмов σ12: R1 → R2, σ23: R2 → R3 и σ13: R1 → R3, удовлетворяющих условию тройки, выполняется σ23(σ12(x)) = σ13(x) для всех x ∈ R1.

LaTeX

$$$\sigma_{23}(\sigma_{12}(x)) = \sigma_{13}(x)$$$

Lean4

@[simp]
theorem comp_apply [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {x : R₁} : σ₂₃ (σ₁₂ x) = σ₁₃ x :=
  RingHom.congr_fun comp_eq x

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