gMul_eq_coe_linearMap — Mathlib

English

Same as the previous, emphasizing the equality of gMul.mul with the linear map obtained from the underlying linear equivalence.

Русский

То же самое, подчеркивающее равенство gMul.mul и линейного отображения, полученного из соответствующего линейного эквивалента.

LaTeX

$$$a ₜ* b = \\text{LinearMap.coe}(\\text{mulEquiv}) (a ⊗ b)$$$

Lean4

theorem gMul_eq_coe_linearMap {i j} (a : ⨂[R]^i M) (b : (⨂[R]^j) M) :
    a ₜ* b =
      ((TensorProduct.mk R _ _).compr₂ ↑(mulEquiv : _ ≃ₗ[R] (⨂[R]^(i + j)) M) :
          ⨂[R]^i M →ₗ[R] (⨂[R]^j) M →ₗ[R] (⨂[R]^(i + j)) M)
        a b :=
  rfl

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