equivariantOfLinearOfComm_apply — Mathlib

English

If v ∈ V, then applying the equivariantOfLinearOfComm construction yields the original k-linear map’s value, i.e. (equivariantOfLinearOfComm f h) v = f v.

Русский

Пусть v ∈ V. Тогда результат применения конструктивного эквивариантного перехода совпадает с исходным значением f: (equivariantOfLinearOfComm f h) v = f v.

LaTeX

$$$ (\\mathrm{equivariantOfLinearOfComm}\\ f\\ h)\\ v = f\\ v $$$

Lean4

@[simp]
theorem equivariantOfLinearOfComm_apply (v : V) : (equivariantOfLinearOfComm f h) v = f v :=
  rfl

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