lTensor_comp_cancelBaseChange — Mathlib

English

LTensor followed by CancelBaseChange equals CancelBaseChange after LTensor; the left action commutes with base-change isomorphism.

Русский

После применения LTensor и CancelBaseChange результат равен CancelBaseChange после LTensor; левая операция совместима с базовым изменением.

LaTeX

$$$lTensor\_{N,Q} \circ \mathrm{cancelBaseChange}_{M,N} = \mathrm{cancelBaseChange}_{Q} \circ lTensor_{M,Q}$$$

Lean4

theorem lTensor_comp_cancelBaseChange (f : N →ₗ[R] Q) :
    lTensor _ _ f ∘ₗ cancelBaseChange R A B M N =
      (cancelBaseChange R A B M Q).toLinearMap ∘ₗ lTensor _ _ (lTensor _ _ f) :=
  by ext; simp

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