Commit 2023-04-10 15:18 53caa18f

View on Github →

feat: port LinearAlgebra.Alternating (#3337)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Alternating.lean

added theorem AlternatingMap.add_apply

added theorem AlternatingMap.add_compLinearMap

added def AlternatingMap.codRestrict

added theorem AlternatingMap.coeFn_smul

added theorem AlternatingMap.coe_add

added theorem AlternatingMap.coe_alternatization

added theorem AlternatingMap.coe_compLinearMap

added theorem AlternatingMap.coe_domDomCongr

added theorem AlternatingMap.coe_inj

added theorem AlternatingMap.coe_injective

added theorem AlternatingMap.coe_mk

added theorem AlternatingMap.coe_multilinearMap

added theorem AlternatingMap.coe_multilinearMap_injective

added theorem AlternatingMap.coe_multilinearMap_mk

added theorem AlternatingMap.coe_neg

added theorem AlternatingMap.coe_smul

added theorem AlternatingMap.coe_sub

added theorem AlternatingMap.coe_zero

added theorem AlternatingMap.compLinearEquiv_eq_zero_iff

added def AlternatingMap.compLinearMap

added theorem AlternatingMap.compLinearMap_apply

added theorem AlternatingMap.compLinearMap_assoc

added theorem AlternatingMap.compLinearMap_id

added theorem AlternatingMap.compLinearMap_inj

added theorem AlternatingMap.compLinearMap_injective

added theorem AlternatingMap.compLinearMap_zero

added theorem AlternatingMap.congr_arg

added theorem AlternatingMap.congr_fun

added def AlternatingMap.constLinearEquivOfIsEmpty

added def AlternatingMap.constOfIsEmpty

added def AlternatingMap.curryLeft

added def AlternatingMap.curryLeftLinearMap

added theorem AlternatingMap.curryLeft_add

added theorem AlternatingMap.curryLeft_compAlternatingMap

added theorem AlternatingMap.curryLeft_compLinearMap

added theorem AlternatingMap.curryLeft_same

added theorem AlternatingMap.curryLeft_smul

added theorem AlternatingMap.curryLeft_zero

added def AlternatingMap.domCoprod'

added theorem AlternatingMap.domCoprod'_apply

added def AlternatingMap.domCoprod.summand

added theorem AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero

added theorem AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant

added theorem AlternatingMap.domCoprod.summand_mk''

added def AlternatingMap.domCoprod

added theorem AlternatingMap.domCoprod_coe

added def AlternatingMap.domDomCongr

added def AlternatingMap.domDomCongrEquiv

added theorem AlternatingMap.domDomCongr_add

added theorem AlternatingMap.domDomCongr_eq_iff

added theorem AlternatingMap.domDomCongr_eq_zero_iff

added theorem AlternatingMap.domDomCongr_perm

added theorem AlternatingMap.domDomCongr_refl

added theorem AlternatingMap.domDomCongr_trans

added theorem AlternatingMap.domDomCongr_zero

added def AlternatingMap.domLCongr

added theorem AlternatingMap.domLCongr_refl

added theorem AlternatingMap.domLCongr_symm

added theorem AlternatingMap.domLCongr_trans

added theorem AlternatingMap.ext

added theorem AlternatingMap.ext_iff

added theorem AlternatingMap.map_add

added theorem AlternatingMap.map_add_swap

added theorem AlternatingMap.map_congr_perm

added theorem AlternatingMap.map_coord_zero

added theorem AlternatingMap.map_eq_zero_of_eq

added theorem AlternatingMap.map_eq_zero_of_not_injective

added theorem AlternatingMap.map_linearDependent

added theorem AlternatingMap.map_neg

added theorem AlternatingMap.map_perm

added theorem AlternatingMap.map_smul

added theorem AlternatingMap.map_sub

added theorem AlternatingMap.map_swap

added theorem AlternatingMap.map_swap_add

added theorem AlternatingMap.map_update_self

added theorem AlternatingMap.map_update_sum

added theorem AlternatingMap.map_update_update

added theorem AlternatingMap.map_update_zero

added theorem AlternatingMap.map_vecCons_add

added theorem AlternatingMap.map_vecCons_smul

added theorem AlternatingMap.map_zero

added theorem AlternatingMap.neg_apply

added def AlternatingMap.ofSubsingleton

added theorem AlternatingMap.smul_apply

added theorem AlternatingMap.sub_apply

added theorem AlternatingMap.toFun_eq_coe

added theorem AlternatingMap.zero_apply

added theorem AlternatingMap.zero_compLinearMap

added structure AlternatingMap

added theorem Basis.ext_alternating

added theorem Equiv.Perm.ModSumCongr.swap_smul_involutive

added theorem LinearMap.coe_compAlternatingMap

added def LinearMap.compAlternatingMap

added theorem LinearMap.compAlternatingMap_apply

added theorem LinearMap.compAlternatingMap_codRestrict

added theorem LinearMap.compMultilinearMap_alternatization

added theorem LinearMap.subtype_compAlternatingMap_codRestrict

added def MultilinearMap.alternatization

added theorem MultilinearMap.alternatization_apply

added theorem MultilinearMap.alternatization_coe

added theorem MultilinearMap.alternatization_def

added theorem MultilinearMap.domCoprod_alternization

added theorem MultilinearMap.domCoprod_alternization_coe

added theorem MultilinearMap.domCoprod_alternization_eq