Mathlib v3 is deprecated. Go to Mathlib v4

Theorem tensor_power.ghas_mul_def

Modification history

2022-05-24 12:33
src/linear_algebra/tensor_power.lean
feat(linear_algebra/tensor_power): Add notation for tensor powers, and a definition of multiplication (#14196) …
Added tensor_power.ghas_mul_defView on Github →