toRingHom_toMonoidHom

Mathlib.Algebra.Algebra.Hom

URI: https://scilib.ai/kg/mathlib#AlgHom.toRingHom_toMonoidHom

English

The canonical equality between the ring hom part of f and the monoid hom part is preserved, i.e., (f : A →+* B) and (f : A →* B) coincide.

Русский

Каноническое равенство междуRingHom и MonoidHom сохраняется: (f : A →+* B) = (f : A →* B).

LaTeX

$$$(f : A \\to+* B) = (f : A \\to* B)$$$

Lean4

@[simp]
theorem toRingHom_toMonoidHom (f : A →ₐ[R] B) : ((f : A →+* B) : A →* B) = f :=
  rfl

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

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

Разделы

Аффилиация

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