gMul_def — Mathlib

English

The graded multiplication defined on tensor powers coincides with the underlying linear map given by the linear equivalence mulEquiv; i.e., a ₜ* b equals the image of a ⊗ b under the corresponding linear map.

Русский

Градуированное умножение на тензорные степени совпадает с линейным отображением, заданным линейным эквивалентом mulEquiv; то есть a ₜ* b является образом a ⊗ b под соответствующей линейной картой.

LaTeX

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

Lean4

theorem gMul_def {i j} (a : ⨂[R]^i M) (b : (⨂[R]^j) M) : a ₜ* b = @mulEquiv R M _ _ _ i j (a ⊗ₜ b) :=
  rfl

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