ext_to_ring

Mathlib.RingTheory.Bialgebra.Hom

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

English

Reiterates that any two bialgebra maps A →ₐc[R] R are equal; rigidity of the target being the ground ring.

Русский

Повторение: любые два биалгебра-гомоморфизма A →ₐc[R] R равны; жесткость целевого объекта — базовое кольцо.

LaTeX

$$ext_to_ring (f g : A →ₐc[R] R) : f = g$$

Lean4

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

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

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

Разделы

Аффилиация

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