congr_trans_rTensor — Mathlib

English

For f' : P ≃ S, f : M ≃ P, g : N ≃ Q, the relation TensorProduct.congr f g ≪≫ₗ f'.rTensor _ = TensorProduct.congr (f ≪≫ₗ f') g holds.

Русский

Для f', f, g выполняется: конгруэнция тензорного произведения композиции равна конгруэнции с объединёнными операциями.

LaTeX

$$$$(\\mathrm{TensorProduct.congr} f g) \\trans (f' \\rTensor _) = \\mathrm{TensorProduct.congr} (f \\trans f') g.$$$$

Lean4

@[simp]
theorem congr_trans_rTensor (f' : P ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
    TensorProduct.congr f g ≪≫ₗ f'.rTensor _ = TensorProduct.congr (f ≪≫ₗ f') g :=
  toLinearMap_injective <| LinearMap.rTensor_comp_map M _ _ _

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