mkRingHom_rel

Mathlib.Algebra.RingQuot

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

English

If x is related to y by the relation r, then their images in the quotient are equal.

Русский

Если x связан с y отношением r, то их образы в остатке равны.

LaTeX

$$$x \; r \; y \Rightarrow \overline{x} = \overline{y}$$$

Lean4

theorem mkRingHom_rel {r : R → R → Prop} {x y : R} (w : r x y) : mkRingHom r x = mkRingHom r y := by
  simp [mkRingHom_def, Quot.sound (Rel.of w)]

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

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

Разделы

Аффилиация

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