algHom_ext

Mathlib.Algebra.Polynomial.AlgebraMap

URI: https://scilib.ai/kg/mathlib#Polynomial.algHom_ext

English

Two R[X]-algebra homomorphisms into B are equal if they agree on the indeterminate X.

Русский

Два гомоморфизма R[X] →_R B совпадают, если совпадают на X.

LaTeX

$$$$f,g:\ R[X] \to_A[R] B\; (f X = g X) \Rightarrow f = g.$$$$

Lean4

@[ext 1200]
theorem algHom_ext {f g : R[X] →ₐ[R] B} (hX : f X = g X) : f = g :=
  algHom_ext' (Subsingleton.elim _ _) hX

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

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

Разделы

Аффилиация

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