toNonUnitalRingHomClass

Mathlib.Algebra.Ring.Equiv

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

← MathLib Explorer

English

From a RingEquivClass, derive a NonUnitalRingHomClass between rings.

Русский

Из RingEquivClass выводят NonUnitalRingHomClass между кольцами.

LaTeX

$$NonUnitalRingHomClass F R S$$

Lean4

instance (priority := 100) toNonUnitalRingHomClass [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S]
    [h : RingEquivClass F R S] : NonUnitalRingHomClass F R S :=
  { h with map_zero := map_zero }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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