congr_arg

Mathlib.Algebra.Module.Equiv.Defs

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

English

Another formulation of equality between semilinear equivalences via their underlying functions.

Русский

Еще одно формулирование равенства семилинейных эквивалентностей через их базовые функции.

LaTeX

$$toFun_eq_coe : e.toFun = EquivLike.toFunLike.coe e$$

Lean4

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

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

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

Разделы

Аффилиация

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