Commit 2024-02-29 12:38 2353c4e3

View on Github →

fix(LinearAlgebra/TensorPower): correct notation precedence (#11062) This removes some ugly parens that were introduced during porting

Estimated changes

Modified Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean

modified def TensorAlgebra.equivDirectSum

modified theorem TensorAlgebra.mk_reindex_cast

modified theorem TensorAlgebra.mk_reindex_fin_cast

modified def TensorAlgebra.ofDirectSum

modified def TensorAlgebra.toDirectSum

modified theorem TensorAlgebra.toDirectSum_ofDirectSum

modified def TensorPower.toTensorAlgebra

Modified Mathlib/LinearAlgebra/TensorPower.lean

modified theorem TensorPower.algebraMap₀_mul

modified def TensorPower.cast

modified theorem TensorPower.cast_cast

modified theorem TensorPower.gMul_def

modified theorem TensorPower.gMul_eq_coe_linearMap

modified def TensorPower.mulEquiv

modified theorem TensorPower.mul_algebraMap₀

modified theorem TensorPower.mul_one

modified theorem TensorPower.one_mul