toNonUnitalRingHomClass

Mathlib.Algebra.Ring.Hom.Defs

URI: https://scilib.ai/kg/mathlib#RingHomClass.toNonUnitalRingHomClass

English

A RingHomClass induces a nonunital ring-hom class structure.

Русский

КлассRingHom порождает структуру NonUnitalRingHomClass.

LaTeX

$$$$ \text{There is a canonical instance } {\text{NonUnitalRingHomClass}}(F, \alpha, \beta) $$$$

Lean4

instance (priority := 100) toNonUnitalRingHomClass : NonUnitalRingHomClass F α β :=
  { ‹RingHomClass F α β› with }

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

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

Разделы

Аффилиация

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