Theorems · Theorem · ring theory

TensorAlgebra.toDirectSum_comp_ofDirectSum

∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorAlgebra.toDirectSum.comp TensorAlgebra.ofDirectSum = AlgHom.id R (DirectSum ℕ fun n => TensorPower R n M)

Defined in

Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Cited by

1 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModule