directLimitRight_tmul_of — Mathlib

English

Tensoring a scalar m with a component g under the right direct limit maps to the corresponding tensor in the directLimit.

Русский

Тензорирование скаляра m с компонентом g в правом прямом пределе переходит в соответствующий тензор в прямом пределе.

LaTeX

$$$\mathrm{directLimitRight}\; f\; M\; (m \otimes g) = \mathrm{in}_i(m \otimes g)$$$

Lean4

@[simp]
theorem directLimitRight_tmul_of {i : ι} (m : M) (g : G i) :
    directLimitRight f M (m ⊗ₜ of _ _ _ _ _ g) = of _ _ _ _ i (m ⊗ₜ g) := by simp [directLimitRight, congr_apply_of]

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