congr_arg

Mathlib.Algebra.Algebra.Hom

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

English

If x = y in A, then φ x = φ y for any AlgHom φ: A →ₐ[R] B.

Русский

Если x = y в A, то φ x = φ y для любого AlgHom φ: A →ₐ[R] B.

LaTeX

$$$x = y \\Rightarrow φ x = φ y$$$

Lean4

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

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

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

Разделы

Аффилиация

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