Commit 2023-04-07 11:39 959d3b90

View on Github →

feat: port LinearAlgebra.Multilinear.Basic (#2450)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Multilinear/Basic.lean

added theorem LinearMap.coe_compMultilinearMap

added def LinearMap.compMultilinearMap

added theorem LinearMap.compMultilinearMap_apply

added theorem LinearMap.compMultilinearMap_codRestrict

added theorem LinearMap.compMultilinearMap_domDomCongr

added theorem LinearMap.curry_uncurryLeft

added theorem LinearMap.subtype_compMultilinearMap_codRestrict

added def LinearMap.uncurryLeft

added theorem LinearMap.uncurryLeft_apply

added theorem MultilinearMap.add_apply

added def MultilinearMap.codRestrict

added theorem MultilinearMap.coe_curr_sum_equiv_symm

added theorem MultilinearMap.coe_currySumEquiv

added theorem MultilinearMap.coe_inj

added theorem MultilinearMap.coe_injective

added theorem MultilinearMap.coe_mk

added theorem MultilinearMap.coe_restrictScalars

added theorem MultilinearMap.coe_smul

added def MultilinearMap.compLinearMap

added theorem MultilinearMap.compLinearMap_apply

added theorem MultilinearMap.compLinearMap_assoc

added theorem MultilinearMap.compLinearMap_id

added theorem MultilinearMap.compLinearMap_inj

added theorem MultilinearMap.compLinearMap_injective

added theorem MultilinearMap.comp_linearEquiv_eq_zero_iff

added theorem MultilinearMap.congr_fun

added theorem MultilinearMap.cons_add

added theorem MultilinearMap.cons_smul

added def MultilinearMap.constLinearEquivOfIsEmpty

added def MultilinearMap.constOfIsEmpty

added def MultilinearMap.curryFinFinset

added theorem MultilinearMap.curryFinFinset_apply

added theorem MultilinearMap.curryFinFinset_apply_const

added theorem MultilinearMap.curryFinFinset_apply_const_aux

added theorem MultilinearMap.curryFinFinset_symm_apply

added theorem MultilinearMap.curryFinFinset_symm_apply_const

added theorem MultilinearMap.curryFinFinset_symm_apply_piecewise_const

added theorem MultilinearMap.curryFinFinset_symm_apply_piecewise_const_aux

added def MultilinearMap.curryLeft

added theorem MultilinearMap.curryLeft_apply

added def MultilinearMap.curryRight

added theorem MultilinearMap.curryRight_apply

added def MultilinearMap.currySum

added def MultilinearMap.currySumEquiv

added theorem MultilinearMap.currySum_apply

added theorem MultilinearMap.curry_uncurryRight

added def MultilinearMap.domDomCongr

added def MultilinearMap.domDomCongrEquiv

added def MultilinearMap.domDomCongrLinearEquiv'

added def MultilinearMap.domDomCongrLinearEquiv

added theorem MultilinearMap.domDomCongr_eq_iff

added theorem MultilinearMap.domDomCongr_mul

added theorem MultilinearMap.domDomCongr_trans

added theorem MultilinearMap.ext

added theorem MultilinearMap.ext_iff

added def MultilinearMap.map

added theorem MultilinearMap.map_add_univ

added theorem MultilinearMap.map_coord_zero

added theorem MultilinearMap.map_neg

added theorem MultilinearMap.map_nonempty

added theorem MultilinearMap.map_piecewise_add

added theorem MultilinearMap.map_piecewise_smul

added theorem MultilinearMap.map_smul_univ

added theorem MultilinearMap.map_sub

added theorem MultilinearMap.map_sum

added theorem MultilinearMap.map_sum_finset

added theorem MultilinearMap.map_sum_finset_aux

added theorem MultilinearMap.map_update_smul

added theorem MultilinearMap.map_update_sum

added theorem MultilinearMap.map_update_zero

added theorem MultilinearMap.map_zero

added theorem MultilinearMap.mkPiAlgebraFin_apply

added theorem MultilinearMap.mkPiAlgebraFin_apply_const

added theorem MultilinearMap.mkPiAlgebra_apply

added theorem MultilinearMap.mkPiRing_apply

added theorem MultilinearMap.mkPiRing_apply_one_eq_self

added theorem MultilinearMap.mkPiRing_eq_iff

added theorem MultilinearMap.mkPiRing_eq_zero_iff

added theorem MultilinearMap.mkPiRing_zero

added theorem MultilinearMap.mk_coe

added theorem MultilinearMap.neg_apply

added def MultilinearMap.ofSubsingleton

added def MultilinearMap.pi

added def MultilinearMap.prod

added def MultilinearMap.range

added def MultilinearMap.restr

added def MultilinearMap.restrictScalars

added def MultilinearMap.smulRight

added theorem MultilinearMap.smulRight_apply

added theorem MultilinearMap.smul_apply

added theorem MultilinearMap.snoc_add

added theorem MultilinearMap.snoc_smul

added theorem MultilinearMap.sub_apply

added theorem MultilinearMap.sum_apply

added theorem MultilinearMap.toFun_eq_coe

added def MultilinearMap.toLinearMap

added def MultilinearMap.uncurryRight

added theorem MultilinearMap.uncurryRight_apply

added def MultilinearMap.uncurrySum

added theorem MultilinearMap.uncurrySum_aux_apply

added theorem MultilinearMap.uncurry_curryLeft

added theorem MultilinearMap.uncurry_curryRight

added theorem MultilinearMap.zero_apply

added theorem MultilinearMap.zero_compLinearMap

added structure MultilinearMap

added def multilinearCurryLeftEquiv

added def multilinearCurryRightEquiv

Modified Mathlib/Logic/Equiv/Set.lean

modified theorem dite_comp_equiv_update