congr_arg

Mathlib.RingTheory.Bialgebra.Hom

URI: https://scilib.ai/kg/mathlib#BialgHom.congr_arg

English

If two arguments x and y are equal, then applying any morphism to them yields equal results.

Русский

Если x = y, то применение морфизма к x и к y даёт равные результаты.

LaTeX

$$$x = y \\Rightarrow \\phi(x) = \\phi(y)$$$

Lean4

protected theorem congr_arg (φ : A →ₐc[R] B) {x y : A} (h : x = y) : φ x = φ y :=
  DFunLike.congr_arg φ h

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

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

Разделы

Аффилиация

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