coe_inj

Mathlib.Algebra.Ring.Hom.Defs

URI: https://scilib.ai/kg/mathlib#RingHom.coe_inj

English

Equality of underlying functions implies equality of RingHoms.

Русский

Равенство функций-основ подводит равенство RingHom.

LaTeX

$$$$ (f : \alpha \to^+_* \beta) = (g : \alpha \to^+_* \beta) \Rightarrow f = g $$$$

Lean4

theorem coe_inj ⦃f g : α →+* β⦄ (h : (f : α → β) = g) : f = g :=
  DFunLike.coe_injective h

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

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

Разделы

Аффилиация

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