ext_of_ring

Mathlib.RingTheory.Bialgebra.Hom

URI: https://scilib.ai/kg/mathlib#BialgHom.ext_of_ring

English

Two algebra morphisms from a ring R to A are equal if they agree on the unit element 1.

Русский

Два алгомоморфизма из кольца R в A равны, если они совпадают на единице 1.

LaTeX

$$$f(1) = g(1) \\Rightarrow f = g$$$

Lean4

@[ext high]
theorem ext_of_ring {f g : R →ₐc[R] A} (h : f 1 = g 1) : f = g :=
  coe_linearMap_injective (by ext; assumption)

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

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

Разделы

Аффилиация

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