Commit 2024-01-10 15:56 3846d4de

View on Github →

feat(LinearAlgebra/PiTensorProduct): make reindex dependently typed (#9445) used to be (⨂[R] _ : ι, M) ≃ₗ[R] ⨂[R] _ : ι₂, M, now M can vary according to the indexing set.

Estimated changes

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean

modified inductive PiTensorProduct.Eqv

modified theorem PiTensorProduct.add_tprodCoeff'

modified theorem PiTensorProduct.add_tprodCoeff

modified def PiTensorProduct.isEmptyEquiv

modified theorem PiTensorProduct.isEmptyEquiv_apply_tprod

modified theorem PiTensorProduct.lift.tprod

modified def PiTensorProduct.liftAddHom

modified theorem PiTensorProduct.liftAux_tprod

modified theorem PiTensorProduct.liftAux_tprodCoeff

modified theorem PiTensorProduct.lift_comp_reindex

added theorem PiTensorProduct.lift_comp_reindex_symm

modified theorem PiTensorProduct.lift_reindex

added theorem PiTensorProduct.lift_reindex_symm

modified def PiTensorProduct.reindex

modified theorem PiTensorProduct.reindex_refl

modified theorem PiTensorProduct.reindex_reindex

modified theorem PiTensorProduct.reindex_symm

modified theorem PiTensorProduct.reindex_tprod

modified theorem PiTensorProduct.smul_tprodCoeff'

modified theorem PiTensorProduct.smul_tprodCoeff

modified theorem PiTensorProduct.smul_tprodCoeff_aux

modified def PiTensorProduct.tprodCoeff

modified theorem PiTensorProduct.tprodCoeff_eq_smul_tprod

modified theorem PiTensorProduct.zero_tprodCoeff'

modified theorem PiTensorProduct.zero_tprodCoeff

Modified Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean

Modified Mathlib/LinearAlgebra/TensorPower.lean

Modified Mathlib/Logic/Equiv/Basic.lean

added theorem Equiv.piCongrLeft'_symm