mkAlgHom_coe

Mathlib.Algebra.RingQuot

URI: https://scilib.ai/kg/mathlib#RingQuot.mkAlgHom_coe

← MathLib Explorer

English

The equality (mkAlgHom S s : A →+* RingQuot s) = mkRingHom s holds.

Русский

Равенство (mkAlgHom S s : A →+* RingQuot s) = mkRingHom s совпадает.

LaTeX

$$$(mkAlgHom S s : A \\to\\+* RingQuot s) = mkRingHom s$$$

Lean4

@[simp]
theorem mkAlgHom_coe (s : A → A → Prop) : (mkAlgHom S s : A →+* RingQuot s) = mkRingHom s :=
  by
  simp_rw [mkAlgHom_def, mkRingHom_def]
  rfl

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

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

Разделы

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

Аффилиация

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