Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi_tensor_product.graded_monoid_eq_of_reindex_cast

Modification history

2023-03-30 18:52
src/linear_algebra/tensor_power.lean
refactor(linear_algebra/{multilinear,pi_tensor_product}): remove the decidable_eq argument (#10140) …
Modified pi_tensor_product.graded_monoid_eq_of_reindex_castView on Github →
2023-03-30 12:15
src/linear_algebra/tensor_power.lean
feat(linear_algebra/tensor_power): the tensor powers form a graded algebra (#10255)
Added pi_tensor_product.graded_monoid_eq_of_reindex_castView on Github →