congr_toLinearEquiv — Mathlib

English

The linearization of the congruence map induced by f and g coincides with the tensor-product congruence on the linearizations f.toLinearEquiv and g.toLinearEquiv.

Русский

Линейное отображение, лежащее в основе конгруэнтности, совпадает с конгруэнтностью тензорного произведения на линейных отображениях f и g.

LaTeX

$$$(\mathrm{congr}(f,g))^{\mathrm{toLinearEquiv}} = \mathrm{congr}(f^{\mathrm{toLinearEquiv}}, g^{\mathrm{toLinearEquiv}})$$

Lean4

@[simp]
theorem congr_toLinearEquiv (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) :
    (Algebra.TensorProduct.congr f g).toLinearEquiv =
      TensorProduct.AlgebraTensorModule.congr f.toLinearEquiv g.toLinearEquiv :=
  rfl

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