instRingHomClass

Mathlib.Algebra.Ring.Hom.Defs

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

← MathLib Explorer

English

The RingHomClass structure for maps α →+* β is defined by its basic map properties.

Русский

Структура RingHomClass задаёт базовые свойства отображений.

LaTeX

$$$$ \text{RingHomClass } (\alpha \to^+* \beta) $$$$

Lean4

instance instRingHomClass : RingHomClass (α →+* β) α β
    where
  map_add := RingHom.map_add'
  map_zero := RingHom.map_zero'
  map_mul f := f.map_mul'
  map_one f := f.map_one'

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

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

Разделы

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

Аффилиация

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