Commit 2023-06-07 03:51 159e04e7

View on Github →

feat: port LinearAlgebra.TensorAlgebra.Basic (#3600)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

added def FreeAlgebra.toTensor

added theorem FreeAlgebra.toTensor_ι

added inductive TensorAlgebra.Rel

added def TensorAlgebra.algebraMapInv

added theorem TensorAlgebra.algebraMap_eq_one_iff

added theorem TensorAlgebra.algebraMap_eq_zero_iff

added theorem TensorAlgebra.algebraMap_inj

added theorem TensorAlgebra.algebraMap_leftInverse

added theorem TensorAlgebra.hom_ext

added theorem TensorAlgebra.induction

added def TensorAlgebra.lift

added theorem TensorAlgebra.lift_comp_ι

added theorem TensorAlgebra.lift_unique

added theorem TensorAlgebra.lift_ι_apply

added theorem TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι

added def TensorAlgebra.toTrivSqZeroExt

added theorem TensorAlgebra.toTrivSqZeroExt_ι

added def TensorAlgebra.tprod

added theorem TensorAlgebra.tprod_apply

added def TensorAlgebra.ιInv

added theorem TensorAlgebra.ι_comp_lift

added theorem TensorAlgebra.ι_eq_algebraMap_iff

added theorem TensorAlgebra.ι_eq_zero_iff

added theorem TensorAlgebra.ι_inj

added theorem TensorAlgebra.ι_leftInverse

added theorem TensorAlgebra.ι_ne_one

added theorem TensorAlgebra.ι_range_disjoint_one

added def TensorAlgebra