ext_to_ring

Mathlib.RingTheory.Coalgebra.Hom

URI: https://scilib.ai/kg/mathlib#Coalgebra.ext_to_ring

English

Two coalgebra morphisms f,g: A →ₗc[R] R are equal if they agree on all inputs; hence extensionality holds.

Русский

Два коалгоморфизма f,g: A →ₗc[R] R равны, если совпадают на всех входах; расширение действует.

LaTeX

$$$f = g$ for all inputs$$

Lean4

@[ext high]
theorem ext_to_ring (f g : A →ₗc[R] R) : f = g :=
  Subsingleton.elim _ _

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

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

Разделы

Аффилиация

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