congr_fun

Mathlib.Algebra.Module.Equiv.Defs

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

English

If x = x', then applying the same semilinear equivalence e yields e x = e x'.

Русский

Если x = x', то применение той же семилинейной эквивалентности e даёт e x = e x'.

LaTeX

$$congr_arg {x x'} : x = x' → e x = e x'$$

Lean4

protected theorem congr_fun (h : e = e') (x : M) : e x = e' x :=
  DFunLike.congr_fun h x

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

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

Разделы

Аффилиация

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