coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero

Mathlib.Algebra.Ring.Hom.Defs

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero

← MathLib Explorer

English

The coercion equality holds for the AddMonoidHom to RingHom construction.

Русский

Сохранение равенства отображений при преобразовании AddMonoidHom в RingHom.

LaTeX

$$$\text{coe}(f) = f$ for the constructed RingHom from AddMonoidHom$$

Lean4

@[simp]
theorem coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero (h h_two h_one) :
    (f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one : β →+ α) = f :=
  by
  ext
  rfl

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

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

Разделы

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

Аффилиация

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