congr_arg

Mathlib.RingTheory.Bialgebra.Equiv

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

English

If x = x′, then e(x) = e(x′) for a bialgebra equivalence e.

Русский

Если x = x′, то e(x) = e(x′) для биалгебрового эквивалентного отображения e.

LaTeX

$$$x=x' \\Rightarrow e(x)=e(x')$$$

Lean4

protected theorem congr_arg {x x'} : x = x' → e x = e x' :=
  DFunLike.congr_arg e

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

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

Разделы

Аффилиация

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