comp_apply

Mathlib.Algebra.Algebra.Hom

URI: https://scilib.ai/kg/mathlib#AlgHom.comp_apply

English

For AlgHoms φ1 : B →ₐ[R] C and φ2 : A →ₐ[R] B, and p ∈ A, (φ1.comp φ2) p = φ1(φ2 p).

Русский

Для гомоморфизмов φ1: B →ₐ[R] C и φ2: A →ₐ[R] B и элемента p ∈ A выполняется (φ1.comp φ2) p = φ1(φ2 p).

LaTeX

$$$\\forall p \\in A, (φ_1.comp φ_2) p = φ_1(φ_2 p)$$$

Lean4

theorem comp_apply (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) (p : A) : φ₁.comp φ₂ p = φ₁ (φ₂ p) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru