Commit 2023-06-03 16:04 39e83849

View on Github →

feat: port LinearAlgebra.PiTensorProduct (#3361)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/PiTensorProduct.lean

added inductive PiTensorProduct.Eqv

added theorem PiTensorProduct.add_tprodCoeff'

added theorem PiTensorProduct.add_tprodCoeff

added theorem PiTensorProduct.ext

added def PiTensorProduct.isEmptyEquiv

added theorem PiTensorProduct.isEmptyEquiv_apply_tprod

added theorem PiTensorProduct.lift.tprod

added theorem PiTensorProduct.lift.unique'

added theorem PiTensorProduct.lift.unique

added def PiTensorProduct.lift

added def PiTensorProduct.liftAddHom

added theorem PiTensorProduct.liftAux.smul

added def PiTensorProduct.liftAux

added theorem PiTensorProduct.liftAux_tprod

added theorem PiTensorProduct.liftAux_tprodCoeff

added theorem PiTensorProduct.lift_comp_reindex

added theorem PiTensorProduct.lift_reindex

added theorem PiTensorProduct.lift_symm

added theorem PiTensorProduct.lift_tprod

added def PiTensorProduct.reindex

added theorem PiTensorProduct.reindex_comp_tprod

added theorem PiTensorProduct.reindex_refl

added theorem PiTensorProduct.reindex_reindex

added theorem PiTensorProduct.reindex_symm

added theorem PiTensorProduct.reindex_tprod

added theorem PiTensorProduct.reindex_trans

added theorem PiTensorProduct.smul_tprodCoeff'

added theorem PiTensorProduct.smul_tprodCoeff

added theorem PiTensorProduct.smul_tprodCoeff_aux

added def PiTensorProduct.subsingletonEquiv

added theorem PiTensorProduct.subsingletonEquiv_apply_tprod

added def PiTensorProduct.tmulEquiv

added theorem PiTensorProduct.tmulEquiv_apply

added theorem PiTensorProduct.tmulEquiv_symm_apply

added def PiTensorProduct.tprod

added def PiTensorProduct.tprodCoeff

added theorem PiTensorProduct.tprodCoeff_eq_smul_tprod

added theorem PiTensorProduct.tprod_eq_tprodCoeff_one

added theorem PiTensorProduct.zero_tprodCoeff'

added theorem PiTensorProduct.zero_tprodCoeff

added def PiTensorProduct