mkAlgHom_rel

Mathlib.Algebra.RingQuot

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

← MathLib Explorer

English

If s x y, then mkAlgHom S s x = mkAlgHom S s y.

Русский

Если s x y, то mkAlgHom S s x = mkAlgHom S s y.

LaTeX

$$$\\forall x,y:\\, A,\\ s\\ x\\ y\\Rightarrow mkAlgHom S s x = mkAlgHom S s y$$$

Lean4

theorem mkAlgHom_rel {s : A → A → Prop} {x y : A} (w : s x y) : mkAlgHom S s x = mkAlgHom S s y := by
  simp [mkAlgHom_def, mkRingHom_def, Quot.sound (Rel.of w)]

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

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

Разделы

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

Аффилиация

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