map_adjoin

Mathlib.Algebra.Algebra.Subalgebra.Lattice

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

English

Two algebra homomorphisms are equal on adjoin R s iff they are equal on s.

Русский

Два алгебра-гомоморфа равны на adjoin_R s тогда и только тогда, когда они равны на s.

LaTeX

$$$\\text{EqOn }(\\phi,\\psi,\\operatorname{adjoin}_R s) \\iff \\text{EqOn }(\\phi,\\psi, s)$$$

Lean4

theorem map_adjoin (φ : A →ₐ[R] B) (s : Set A) : (adjoin R s).map φ = adjoin R (φ '' s) :=
  (adjoin_image _ _ _).symm

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

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

Разделы

Аффилиация

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