Mathlib v3 is deprecated. Go to Mathlib v4

Theorem tensor_power.list_prod_graded_monoid_mk_single

Modification history

2023-03-30 12:15
src/linear_algebra/tensor_algebra/to_tensor_power.lean
feat(linear_algebra/tensor_power): the tensor powers form a graded algebra (#10255)
Added tensor_power.list_prod_graded_monoid_mk_singleView on Github →