ext_of_ring

Mathlib.RingTheory.Coalgebra.Hom

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

English

Two coalgebra endomorphisms of R-algebra A are equal if they agree on 1

Русский

Два эндоморфизма коалгебры над R-алгеброй A равны, если они совпадают на единице

LaTeX

$$$$ \text{If } f(1) = g(1) \text{ then } 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