TheoremsbaseChange_inv, baseChange_mul, baseChange_one, baseChange_pow, baseChange_symm, baseChange_tmul, baseChange_trans, baseChange_zpow, coe_baseChange, baseChangeHom_apply, baseChange_add, baseChange_baseChange, baseChange_comp, baseChange_eq_ltensor, baseChange_id, baseChange_mul, baseChange_neg, baseChange_one, baseChange_pow, baseChange_smul, baseChange_sub, baseChange_tmul, baseChange_zero, rTensor_baseChange, baseChangeHom_apply_apply, baseChange_bot, baseChange_eq_span, baseChange_span, baseChange_top, tmul_mem_baseChange_of_mem, assoc_eq, assoc_symm_tmul, assoc_tmul, cancelBaseChange_symm_tmul, cancelBaseChange_tmul, coe_lTensor, coe_rTensor, congr_eq, congr_mul, congr_one, congr_refl, congr_symm, congr_symm_tmul, congr_tmul, congr_trans, curry_apply, curry_injective, curry_injective_iff, ext, homTensorHomMap_apply, lTensor_comp, lTensor_comp_cancelBaseChange, lTensor_id, lTensor_mul, lTensor_one, lTensor_tmul, lcurry_apply, leftComm_eq, leftComm_symm_tmul, leftComm_tmul, lift_apply, lift_tmul, mapBilinear_apply, map_add_left, map_add_right, map_comp, map_eq, map_id, map_mul, map_one, map_smul_left, map_smul_right, map_tmul, mk_apply, rTensor_comp, rTensor_id, rTensor_mul, rTensor_one, rTensor_tensor, rTensor_tmul, restrictScalars_curry, restrictScalars_lTensor, restrictScalars_rTensor, rid_eq_rid, rid_symm_apply, rid_tmul, rightComm_eq, rightComm_symm, rightComm_symm_tmul, rightComm_tmul, smul_eq_lsmul_rTensor, tensorTensorTensorComm_eq, tensorTensorTensorComm_symm, tensorTensorTensorComm_symm_tmul, tensorTensorTensorComm_tmul, uncurry_apply | 96 |