directLimitLeft_rTensor_of — Mathlib

English

Compatibility of directLimitLeft with the rTensor operation on the right: the left limit commutes with rTensor when applied to a pure tensor.

Русский

Совместимость directLimitLeft с rTensor справа: левый предел коммутирует с rTensor при действии на чистый тензор.

LaTeX

$$$\text{directLimitLeft}\;f\;M\; (g \otimes_R m) = \mathrm{in}_i( g) \otimes_R m$$$

Lean4

theorem directLimitLeft_rTensor_of {i : ι} (x : G i ⊗[R] M) :
    directLimitLeft f M (LinearMap.rTensor M (of ..) x) = of _ _ _ (f ▷ M) _ x :=
  x.induction_on (by simp) (by simp +contextual) (by simp +contextual)

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