Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-30 12:15 d97a0c9f

View on Github →

feat(linear_algebra/tensor_power): the tensor powers form a graded algebra (#10255)

Estimated changes

Modified src/data/fin/tuple/basic.lean

added theorem fin.append_left_eq_cons

added theorem fin.append_right_eq_snoc

Created src/linear_algebra/tensor_algebra/to_tensor_power.lean

added def tensor_algebra.equiv_direct_sum

added theorem tensor_algebra.mk_reindex_cast

added theorem tensor_algebra.mk_reindex_fin_cast

added def tensor_algebra.of_direct_sum

added theorem tensor_algebra.of_direct_sum_comp_to_direct_sum

added theorem tensor_algebra.of_direct_sum_of_tprod

added theorem tensor_algebra.of_direct_sum_to_direct_sum

added def tensor_algebra.to_direct_sum

added theorem tensor_algebra.to_direct_sum_comp_of_direct_sum

added theorem tensor_algebra.to_direct_sum_of_direct_sum

added theorem tensor_algebra.to_direct_sum_tensor_power_tprod

added theorem tensor_algebra.to_direct_sum_ι

added theorem tensor_power.list_prod_graded_monoid_mk_single

added def tensor_power.to_tensor_algebra

added theorem tensor_power.to_tensor_algebra_galgebra_to_fun

added theorem tensor_power.to_tensor_algebra_ghas_mul

added theorem tensor_power.to_tensor_algebra_ghas_one

added theorem tensor_power.to_tensor_algebra_tprod

Modified src/linear_algebra/tensor_power.lean

added theorem pi_tensor_product.graded_monoid_eq_of_reindex_cast

added def tensor_power.algebra_map₀

added theorem tensor_power.algebra_map₀_eq_smul_one

added theorem tensor_power.algebra_map₀_mul

added theorem tensor_power.algebra_map₀_mul_algebra_map₀

added theorem tensor_power.algebra_map₀_one

added def tensor_power.cast

added theorem tensor_power.cast_cast

added theorem tensor_power.cast_eq_cast

added theorem tensor_power.cast_refl

added theorem tensor_power.cast_symm

added theorem tensor_power.cast_tprod

added theorem tensor_power.cast_trans

added theorem tensor_power.galgebra_to_fun_def

added theorem tensor_power.ghas_mul_eq_coe_linear_map

modified theorem tensor_power.ghas_one_def

added theorem tensor_power.graded_monoid_eq_of_cast

added theorem tensor_power.mul_algebra_map₀

added theorem tensor_power.mul_assoc

added theorem tensor_power.mul_one

added theorem tensor_power.one_mul

added theorem tensor_power.tprod_mul_tprod