Basic

📁 Source: Mathlib/LinearAlgebra/Multilinear/Basic.lean

Statistics

Metric	Count
Definitions `multilinearMapCongrLeft`, `multilinearMapCongrRight`, `compMultilinearMap`, `compMultilinearMapₗ`, `MultilinearMap`, `addCommMonoid`, `codRestrict`, `coeAddMonoidHom`, `compLinearMap`, `compLinearMapMultilinear`, `compLinearMapₗ`, `compMultilinearMap`, `constLinearEquivOfIsEmpty`, `constOfIsEmpty`, `domDomCongr`, `domDomCongrEquiv`, `domDomCongrLinearEquiv`, `domDomCongrLinearEquiv'`, `domDomRestrict`, `domDomRestrictₗ`, `instAdd`, `instAddCommGroup`, `instDistribMulActionOfSMulCommClass`, `instFunLikeForall`, `instInhabited`, `instModule`, `instNeg`, `instSMul`, `instSub`, `instZero`, `iteratedFDeriv`, `iteratedFDerivComponent`, `linearDeriv`, `map`, `mk'`, `mkPiAlgebra`, `mkPiAlgebraFin`, `mkPiRing`, `ofSubsingleton`, `ofSubsingletonₗ`, `pi`, `piLinearMap`, `piRingEquiv`, `prod`, `range`, `restr`, `restrictScalars`, `smulRight`, `toFun`, `toLinearMap`	50
Theorems `multilinearMapCongrLeft_apply`, `multilinearMapCongrLeft_symm_apply`, `multilinearMapCongrRight_apply`, `multilinearMapCongrRight_symm_apply`, `add_compMultilinearMap`, `coe_compMultilinearMap`, `compMultilinearMap_add`, `compMultilinearMap_apply`, `compMultilinearMap_codRestrict`, `compMultilinearMap_compLinearMap`, `compMultilinearMap_domDomCongr`, `compMultilinearMap_smul`, `compMultilinearMap_zero`, `compMultilinearMapₗ_apply`, `comp_compMultilinearMap`, `id_compMultilinearMap`, `smul_compMultilinearMap`, `subtype_compMultilinearMap_codRestrict`, `zero_compMultilinearMap`, `add_apply`, `codRestrict_apply_coe`, `coeAddMonoidHom_apply`, `coe_inj`, `coe_injective`, `coe_mk`, `coe_restrictScalars`, `coe_smul`, `coe_sum`, `compLinearMapMultilinear_apply`, `compLinearMap_apply`, `compLinearMap_assoc`, `compLinearMap_id`, `compLinearMap_inj`, `compLinearMap_injective`, `compLinearMapₗ_apply`, `compMultilinearMap_apply`, `comp_linearEquiv_eq_zero_iff`, `congr_arg`, `congr_fun`, `cons_add`, `cons_smul`, `constLinearEquivOfIsEmpty_apply`, `constLinearEquivOfIsEmpty_symm_apply`, `constOfIsEmpty_apply`, `domDomCongrEquiv_apply`, `domDomCongrEquiv_symm_apply`, `domDomCongrLinearEquiv'_apply`, `domDomCongrLinearEquiv'_symm_apply`, `domDomCongrLinearEquiv_apply`, `domDomCongrLinearEquiv_symm_apply`, `domDomCongr_apply`, `domDomCongr_eq_iff`, `domDomCongr_mul`, `domDomCongr_trans`, `domDomRestrict_apply`, `domDomRestrict_aux`, `domDomRestrict_aux_right`, `ext`, `ext_iff`, `ext_ring`, `ext_ring_iff`, `instIsTorsionFree`, `iteratedFDeriv_aux`, `linearDeriv_apply`, `map_add_eq_map_add_linearDeriv_add`, `map_add_sub_map_add_sub_linearDeriv`, `map_add_univ`, `map_coord_zero`, `map_insertNth_add`, `map_insertNth_smul`, `map_nonempty`, `map_piecewise_add`, `map_piecewise_smul`, `map_piecewise_sub_map_piecewise`, `map_smul_univ`, `map_sub_map_piecewise`, `map_sum`, `map_sum_finset`, `map_sum_finset_aux`, `map_update`, `map_update_add`, `map_update_add'`, `map_update_neg`, `map_update_smul`, `map_update_smul'`, `map_update_smul_left`, `map_update_sub`, `map_update_sum`, `map_update_zero`, `map_zero`, `mk'_apply`, `mkPiAlgebraFin_apply`, `mkPiAlgebraFin_apply_const`, `mkPiAlgebra_apply`, `mkPiRing_apply`, `mkPiRing_apply_one_eq_self`, `mkPiRing_eq_iff`, `mkPiRing_eq_zero_iff`, `mkPiRing_zero`, `mk_coe`, `neg_apply`, `ofSubsingleton_apply_apply`, `ofSubsingleton_symm_apply_apply`, `ofSubsingletonₗ_apply`, `ofSubsingletonₗ_symm_apply`, `piLinearMap_apply_apply_apply`, `pi_apply`, `prod_apply`, `smulRight_apply`, `smul_apply`, `snoc_add`, `snoc_smul`, `sub_apply`, `sum_apply`, `toFun_eq_coe`, `toLinearMap_apply`, `zero_apply`, `zero_compLinearMap`	118
Total	168

LinearEquiv

Definitions

Name	Category	Theorems
`multilinearMapCongrLeft` 📖	CompOp	3 math math: `multilinearMapCongrLeft_symm_apply`, `MultilinearMap.freeFinsuppEquiv_def`, `multilinearMapCongrLeft_apply`
`multilinearMapCongrRight` 📖	CompOp	3 math math: `multilinearMapCongrRight_apply`, `multilinearMapCongrRight_symm_apply`, `MultilinearMap.freeFinsuppEquiv_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multilinearMapCongrLeft_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `MultilinearMap.addCommMonoid` `MultilinearMap.instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `instEquivLike` `multilinearMapCongrLeft` `MultilinearMap.compLinearMap` `toLinearMap`	—	`RingHomInvPair.ids` `smulCommClass_self`
`multilinearMapCongrLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `MultilinearMap.addCommMonoid` `MultilinearMap.instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `instEquivLike` `symm` `multilinearMapCongrLeft` `MultilinearMap.compLinearMap` `toLinearMap`	—	`RingHomInvPair.ids` `smulCommClass_self`
`multilinearMapCongrRight_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `MultilinearMap.addCommMonoid` `MultilinearMap.instModule` `EquivLike.toFunLike` `instEquivLike` `multilinearMapCongrRight` `LinearMap.compMultilinearMap` `toLinearMap`	—	`RingHomInvPair.ids`
`multilinearMapCongrRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `MultilinearMap.addCommMonoid` `MultilinearMap.instModule` `EquivLike.toFunLike` `instEquivLike` `symm` `multilinearMapCongrRight` `LinearMap.compMultilinearMap` `toLinearMap`	—	`RingHomInvPair.ids`

LinearMap

Definitions

Name	Category	Theorems
`compMultilinearMap` 📖	CompOp	26 math math: `LinearEquiv.multilinearMapCongrRight_apply`, `compMultilinearMap_add`, `compMultilinearMap_compLinearMap`, `smul_compMultilinearMap`, `PiTensorProduct.reindex_comp_tprod`, `compMultilinearMap_alternatization`, `compMultilinearMap_domDomCongr`, `compMultilinearMap_codRestrict`, `MultilinearMap.dfinsuppFamily_compLinearMap_lsingle`, `LinearEquiv.multilinearMapCongrRight_symm_apply`, `zero_compMultilinearMap`, `add_compMultilinearMap`, `compMultilinearMapₗ_apply`, `coe_compMultilinearMap`, `PiTensorProduct.ext_iff`, `compMultilinearMap_smul`, `MultilinearMap.piFamily_single_left`, `compMultilinearMap_zero`, `subtype_compMultilinearMap_codRestrict`, `Basis.multilinearMap_apply`, `MultilinearMap.dfinsuppFamily_single_left`, `MultilinearMap.piFamily_compLinearMap_lsingle`, `compMultilinearMap_apply`, `comp_compMultilinearMap`, `id_compMultilinearMap`, `PiTensorProduct.lift_symm`
`compMultilinearMapₗ` 📖	CompOp	1 math math: `compMultilinearMapₗ_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_compMultilinearMap` 📖	mathematical	—	`compMultilinearMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instAdd` `MultilinearMap` `MultilinearMap.instAdd`	—	—
`coe_compMultilinearMap` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `MultilinearMap.instFunLikeForall` `compMultilinearMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	—	—
`compMultilinearMap_add` 📖	mathematical	—	`compMultilinearMap` `MultilinearMap` `MultilinearMap.instAdd`	—	`MultilinearMap.ext` `map_add` `SemilinearMapClass.toAddHomClass` `semilinearMapClass`
`compMultilinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `MultilinearMap.instFunLikeForall` `compMultilinearMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	—	—
`compMultilinearMap_codRestrict` 📖	mathematical	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	`compMultilinearMap` `Submodule.addCommMonoid` `Submodule.module` `codRestrict` `MultilinearMap.codRestrict` `MultilinearMap` `MultilinearMap.instFunLikeForall`	—	—
`compMultilinearMap_compLinearMap` 📖	mathematical	—	`compMultilinearMap` `MultilinearMap.compLinearMap`	—	—
`compMultilinearMap_domDomCongr` 📖	mathematical	—	`MultilinearMap.domDomCongr` `compMultilinearMap`	—	`MultilinearMap.ext`
`compMultilinearMap_smul` 📖	mathematical	—	`compMultilinearMap` `MultilinearMap` `MultilinearMap.instSMul`	—	`MultilinearMap.ext` `map_smul_of_tower`
`compMultilinearMap_zero` 📖	mathematical	—	`compMultilinearMap` `MultilinearMap` `MultilinearMap.instZero`	—	`MultilinearMap.ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass`
`compMultilinearMapₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MultilinearMap` `MultilinearMap.addCommMonoid` `MultilinearMap.instModule` `instFunLike` `compMultilinearMapₗ` `compMultilinearMap`	—	—
`comp_compMultilinearMap` 📖	mathematical	—	`compMultilinearMap` `comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids`
`id_compMultilinearMap` 📖	mathematical	—	`compMultilinearMap` `id`	—	—
`smul_compMultilinearMap` 📖	mathematical	—	`compMultilinearMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instSMul` `DistribMulAction.toDistribSMul` `AddCommMonoid.toAddMonoid` `MultilinearMap` `MultilinearMap.instSMul`	—	—
`subtype_compMultilinearMap_codRestrict` 📖	mathematical	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `MultilinearMap` `MultilinearMap.instFunLikeForall`	`compMultilinearMap` `Submodule.addCommMonoid` `Submodule.module` `Submodule.subtype` `MultilinearMap.codRestrict`	—	—
`zero_compMultilinearMap` 📖	mathematical	—	`compMultilinearMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instZero` `MultilinearMap` `MultilinearMap.instZero`	—	—

MultilinearMap

Definitions

Name	Category	Theorems
`addCommMonoid` 📖	CompOp	91 math math: `LinearEquiv.multilinearMapCongrLeft_symm_apply`, `domDomCongrLinearEquiv'_symm_apply`, `PiTensorProduct.lift_reindex`, `LinearEquiv.multilinearMapCongrRight_apply`, `PiTensorProduct.lift.tprod`, `fromDFinsuppEquiv_apply`, `PiTensorProduct.liftAlgHom_apply`, `Module.Finite.multilinearMap`, `PiTensorProduct.lift_reindex_symm`, `currySum_add`, `AlternatingMap.domCoprod_coe`, `currySumEquiv_apply`, `PiTensorProduct.toDualContinuousMultilinearMap_apply_apply`, `fromDirectSumEquiv_symm_apply`, `domDomCongrLinearEquiv_symm_apply`, `currySum_apply'`, `PiTensorProduct.reindex_comp_tprod`, `Module.Free.multilinearMap`, `curryFinFinset_apply`, `coe_sum`, `LinearEquiv.multilinearMapCongrRight_symm_apply`, `coe_currySumEquiv_symm`, `curryFinFinset_symm_apply_piecewise_const`, `domCoprod_alternization_coe`, `fromDFinsuppEquiv_single`, `OrderedFinpartition.compAlongOrderedFinpartitionₗ_apply_apply`, `PiTensorProduct.norm_eval_le_injectiveSeminorm`, `PiTensorProduct.liftEquiv_symm_apply`, `AlternatingMap.curryLeft_apply_toMultilinearMap`, `domDomCongrLinearEquiv_apply`, `freeDFinsuppEquiv_single`, `PiTensorProduct.liftEquiv_apply`, `curryMid_apply_apply`, `freeDFinsuppEquiv_def`, `PiTensorProduct.lift_comp_reindex`, `LinearMap.compMultilinearMapₗ_apply`, `LinearMap.uncurryMid_apply`, `curryFinFinset_apply_const`, `freeFinsuppEquiv_def`, `fromDirectSumEquiv_lof`, `domCoprod'_apply`, `instIsTorsionFree`, `curryLeft_apply`, `Basis.multilinearMap_apply_apply`, `dfinsuppFamilyₗ_apply`, `multilinearCurryLeftEquiv_apply`, `constLinearEquivOfIsEmpty_apply`, `curryFinFinset_symm_apply_const`, `domDomCongrLinearEquiv'_apply`, `freeFinsuppEquiv_apply`, `ofSubsingletonₗ_apply`, `piFamilyₗ_apply`, `fromDirectSumEquiv_apply`, `freeFinsuppEquiv_single`, `freeDFinsuppEquiv_apply`, `curryMidLinearEquiv_apply`, `PiTensorProduct.lift_tprod`, `PiTensorProduct.liftIsometry_apply_apply`, `uncurrySum_add`, `PiTensorProduct.norm_eval_le_projectiveSeminorm`, `alternatization_coe`, `PiTensorProduct.lift_comp_map`, `multilinearCurryLeftEquiv_symm_apply`, `piLinearMap_apply_apply_apply`, `coe_currySumEquiv`, `uncurrySum_apply`, `curryMidLinearEquiv_symm_apply`, `Basis.multilinearMap_apply`, `PiTensorProduct.lift.unique'`, `PiTensorProduct.lift_comp_reindex_symm`, `constLinearEquivOfIsEmpty_symm_apply`, `compLinearMapMultilinear_apply`, `currySum_smul`, `sum_apply`, `curryFinFinset_symm_apply`, `AlternatingMap.domCoprod_apply`, `PiTensorProduct.lift.unique`, `ContinuousMultilinearMap.toMultilinearMapLinear_apply`, `LinearEquiv.multilinearMapCongrLeft_apply`, `domCoprodDep'_apply`, `uncurrySum_smul`, `compLinearMapₗ_apply`, `fromDFinsuppEquiv_symm_apply`, `AlternatingMap.toMultilinearMapLM_apply`, `LinearMap.uncurryLeft_apply`, `ofSubsingletonₗ_symm_apply`, `alternatization_def`, `currySumEquiv_symm_apply`, `coeAddMonoidHom_apply`, `currySum_apply`, `PiTensorProduct.lift_symm`
`codRestrict` 📖	CompOp	4 math math: `LinearMap.compMultilinearMap_codRestrict`, `codRestrict_apply_coe`, `ContinuousMultilinearMap.codRestrict_toMultilinearMap`, `LinearMap.subtype_compMultilinearMap_codRestrict`
`coeAddMonoidHom` 📖	CompOp	1 math math: `coeAddMonoidHom_apply`
`compLinearMap` 📖	CompOp	22 math math: `LinearEquiv.multilinearMapCongrLeft_symm_apply`, `compLinearMap_injective`, `LinearMap.compMultilinearMap_compLinearMap`, `fromDirectSumEquiv_symm_apply`, `dfinsuppFamily_compLinearMap_lsingle`, `zero_compLinearMap`, `compLinearMap_id`, `dfinsupp_ext_iff`, `piFamily_single_left`, `comp_linearEquiv_eq_zero_iff`, `directSum_ext_iff`, `PiTensorProduct.lift_comp_map`, `compLinearMap_inj`, `Basis.multilinearMap_apply`, `compLinearMap_apply`, `pi_ext_iff`, `dfinsuppFamily_single_left`, `piFamily_compLinearMap_lsingle`, `LinearEquiv.multilinearMapCongrLeft_apply`, `compLinearMapₗ_apply`, `fromDFinsuppEquiv_symm_apply`, `compLinearMap_assoc`
`compLinearMapMultilinear` 📖	CompOp	1 math math: `compLinearMapMultilinear_apply`
`compLinearMapₗ` 📖	CompOp	2 math math: `compLinearMapMultilinear_apply`, `compLinearMapₗ_apply`
`compMultilinearMap` 📖	CompOp	1 math math: `compMultilinearMap_apply`
`constLinearEquivOfIsEmpty` 📖	CompOp	2 math math: `constLinearEquivOfIsEmpty_apply`, `constLinearEquivOfIsEmpty_symm_apply`
`constOfIsEmpty` 📖	CompOp	3 math math: `ContinuousMultilinearMap.constOfIsEmpty_toMultilinearMap`, `constOfIsEmpty_apply`, `constLinearEquivOfIsEmpty_apply`
`domDomCongr` 📖	CompOp	16 math math: `AlternatingMap.domCoprod.summand_mk''`, `domDomCongrEquiv_symm_apply`, `ContinuousMultilinearMap.domDomCongr_toMultilinearMap`, `domDomCongr_trans`, `LinearMap.compMultilinearMap_domDomCongr`, `domCoprod_alternization_coe`, `domCoprod_domDomCongr_sumCongr`, `AlternatingMap.coe_domDomCongr`, `alternatization_apply`, `domDomCongr_eq_iff`, `alternatization_coe`, `domDomCongr_mul`, `SymmetricPower.domDomCongr_tprod`, `alternatization_def`, `domDomCongr_apply`, `domDomCongrEquiv_apply`
`domDomCongrEquiv` 📖	CompOp	4 math math: `domDomCongrEquiv_symm_apply`, `domDomCongrLinearEquiv_symm_apply`, `domDomCongrLinearEquiv_apply`, `domDomCongrEquiv_apply`
`domDomCongrLinearEquiv` 📖	CompOp	2 math math: `domDomCongrLinearEquiv_symm_apply`, `domDomCongrLinearEquiv_apply`
`domDomCongrLinearEquiv'` 📖	CompOp	7 math math: `domDomCongrLinearEquiv'_symm_apply`, `PiTensorProduct.lift_reindex`, `PiTensorProduct.lift_reindex_symm`, `PiTensorProduct.reindex_comp_tprod`, `PiTensorProduct.lift_comp_reindex`, `domDomCongrLinearEquiv'_apply`, `PiTensorProduct.lift_comp_reindex_symm`
`domDomRestrict` 📖	CompOp	1 math math: `domDomRestrict_apply`
`domDomRestrictₗ` 📖	CompOp	—
`instAdd` 📖	CompOp	13 math math: `LinearMap.compMultilinearMap_add`, `currySum_add`, `piFamily_add`, `add_apply`, `ContinuousMultilinearMap.toMultilinearMap_add`, `domDomCongrEquiv_symm_apply`, `domDomCongrLinearEquiv_symm_apply`, `dfinsuppFamily_add`, `domDomCongrLinearEquiv_apply`, `LinearMap.add_compMultilinearMap`, `uncurrySum_add`, `AlternatingMap.coe_add`, `domDomCongrEquiv_apply`
`instAddCommGroup` 📖	CompOp	10 math math: `AlternatingMap.domCoprod.summand_mk''`, `LinearMap.compMultilinearMap_alternatization`, `domCoprod_alternization_coe`, `domCoprod_alternization_eq`, `alternatization_apply`, `AlternatingMap.coe_alternatization`, `domCoprod_alternization`, `ContinuousMultilinearMap.alternatization_apply_toAlternatingMap`, `alternatization_coe`, `alternatization_def`
`instDistribMulActionOfSMulCommClass` 📖	CompOp	17 math math: `currySumEquiv_apply`, `curryFinFinset_apply`, `coe_currySumEquiv_symm`, `curryFinFinset_symm_apply_piecewise_const`, `curryFinFinset_apply_const`, `multilinearCurryLeftEquiv_apply`, `curryFinFinset_symm_apply_const`, `curryMidLinearEquiv_apply`, `multilinearCurryLeftEquiv_symm_apply`, `piLinearMap_apply_apply_apply`, `coe_currySumEquiv`, `curryMidLinearEquiv_symm_apply`, `compLinearMapMultilinear_apply`, `currySum_smul`, `curryFinFinset_symm_apply`, `uncurrySum_smul`, `currySumEquiv_symm_apply`
`instFunLikeForall` 📖	CompOp	187 math math: `map_piecewise_smul`, `domDomCongrLinearEquiv'_symm_apply`, `TensorAlgebra.ofDirectSum_of_tprod`, `PiTensorProduct.lift.tprod`, `fromDFinsuppEquiv_apply`, `map_update_smul`, `PiTensorProduct.tmulEquiv_symm_apply`, `map_update_add`, `PiTensorProduct.isEmptyEquiv_apply_tprod`, `mkPiAlgebra_apply`, `FreeAddMonoid.toPiTensorProduct`, `dfinsuppFamily_single`, `PiTensorProduct.ofDirectSumEquiv_tprod_lof`, `map_insertNth_add`, `ContinuousMultilinearMap.coe_coe`, `PiTensorProduct.subsingletonEquiv_symm_apply`, `TensorAlgebra.toDirectSum_tensorPower_tprod`, `add_apply`, `coe_restrictScalars`, `smul_apply`, `SemiconjBy.tprod`, `congr_fun`, `map_sum`, `map_insertNth_smul`, `map_update`, `map_piecewise_sub_map_piecewise`, `dfinsuppFamily_apply_toFun`, `dfinsuppFamily_apply_support'`, `coe_inj`, `curryRight_apply`, `currySum_apply'`, `PiTensorProduct.tprod_prod`, `PiTensorProduct.ofFinsuppEquiv'_tprod_single`, `curryFinFinset_apply`, `PiTensorProduct.subsingletonEquiv_apply_tprod`, `coe_sum`, `LinearMap.compMultilinearMap_codRestrict`, `PiTensorProduct.projectiveSeminorm_tprod_le`, `PiTensorProduct.ofDirectSumEquiv_symm_lof_tprod`, `PiTensorProduct.tprodL_toFun`, `PiTensorProduct.ofFinsuppEquiv_tprod_single`, `PiTensorProduct.congr_symm_tprod`, `PiTensorProduct.constantBaseRingEquiv_tprod`, `domCoprodDep_apply`, `SymmetricPower.span_tprod_eq_top`, `curryFinFinset_symm_apply_piecewise_const`, `PiTensorProduct.ofFinsuppEquiv_symm_single_tprod`, `PiTensorProduct.one_def`, `PiTensorProduct.reindex_tprod`, `PiTensorProduct.tprodMonoidHom_apply`, `PiTensorProduct.piTensorHomMap_tprod_tprod`, `map_update_smul_left`, `fromDFinsuppEquiv_single`, `constOfIsEmpty_apply`, `OrderedFinpartition.compAlongOrderedFinpartitionₗ_apply_apply`, `PiTensorProduct.tprodCoeff_eq_smul_tprod`, `TensorPower.tprod_mul_tprod`, `AlternatingMap.coe_mk`, `map_update_neg`, `compMultilinearMap_apply`, `freeDFinsuppEquiv_single`, `map_zero`, `map_add_sub_map_add_sub_linearDeriv`, `PiTensorProduct.liftAux_tprodCoeff`, `curryMid_apply_apply`, `PiTensorProduct.ofDFinsuppEquiv_tprod_apply`, `PiTensorProduct.dualDistribInvOfBasis_apply`, `coe_mk`, `map_sum_finset_aux`, `PiTensorProduct.piTensorHomMap_tprod_eq_map`, `PiTensorProduct.singleAlgHom_apply`, `TensorPower.multilinearMapToDual_apply_tprod`, `PiTensorProduct.map₂_tprod_tprod`, `LinearMap.uncurryMid_apply`, `curryFinFinset_apply_const`, `map_update_sub`, `LinearMap.coe_compMultilinearMap`, `PiTensorProduct.ofFinsuppEquiv_apply`, `cons_add`, `coe_smul`, `fromDirectSumEquiv_lof`, `PiTensorProduct.mapMultilinear_apply`, `PiTensorProduct.dualDistrib_apply`, `curryLeft_apply`, `map_update_zero`, `PiTensorProduct.tprod_eq_tprodCoeff_one`, `Basis.multilinearMap_apply_apply`, `PiTensorProduct.isEmptyEquiv_symm_apply`, `PiTensorProduct.subsingletonEquiv_symm_apply'`, `map_add_eq_map_add_linearDeriv_add`, `PiTensorProduct.tmulEquivDep_symm_apply`, `piFamily_apply`, `PiTensorProduct.liftAux_tprod`, `cons_smul`, `curryFinFinset_symm_apply_const`, `PiTensorProduct.piTensorHomMap₂_tprod_tprod_tprod`, `dfinsuppFamily_single_left_apply`, `domDomCongrLinearEquiv'_apply`, `PiTensorProduct.tmulEquivDep_apply`, `freeFinsuppEquiv_apply`, `map_piecewise_add`, `alternatization_apply`, `fromDirectSumEquiv_apply`, `smulRight_apply`, `PiTensorProduct.mem_lifts_iff`, `PiTensorProduct.ofDFinsuppEquiv_tprod_single`, `sub_apply`, `PiTensorProduct.map_tprod`, `piFamily_single_left_apply`, `domDomRestrict_apply`, `mkPiAlgebraFin_apply`, `TensorPower.list_prod_gradedMonoid_mk_single`, `freeFinsuppEquiv_single`, `PiTensorProduct.one_mul`, `map_coord_zero`, `mkPiRing_apply_one_eq_self`, `ext_ring_iff`, `domCoprod_apply`, `PiTensorProduct.tprod_noncommProd`, `freeDFinsuppEquiv_apply`, `uncurryRight_apply`, `PiTensorProduct.mul_one`, `PiTensorProduct.tmulEquiv_apply`, `TensorAlgebra.tprod_apply`, `TensorPower.cast_tprod`, `PiTensorProduct.mul_tprod_tprod`, `ofSubsingleton_symm_apply_apply`, `AlternatingMap.coe_multilinearMap`, `PiTensorProduct.tprodL_apply`, `support_dfinsuppFamily_subset`, `AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant`, `TensorPower.gOne_def`, `snoc_add`, `neg_apply`, `ext_iff`, `map_sum_finset`, `piLinearMap_apply_apply_apply`, `toFun_eq_coe`, `uncurrySum_apply`, `Commute.tprod`, `PiTensorProduct.ofFinsuppEquiv'_apply_apply`, `piFamily_single`, `compLinearMap_apply`, `SymmetricPower.tprod_equiv`, `mkPiAlgebraFin_apply_const`, `PiTensorProduct.ofDFinsuppEquiv_symm_single_tprod`, `linearDeriv_apply`, `PiTensorProduct.span_tprod_eq_top`, `mkPiRing_apply`, `map_smul_univ`, `toLinearMap_apply`, `constLinearEquivOfIsEmpty_symm_apply`, `compLinearMapMultilinear_apply`, `TensorAlgebra.toDirectSum_ι`, `sum_apply`, `PiTensorProduct.ofDirectSumEquiv_tprod_apply`, `PiTensorProduct.injectiveSeminorm_tprod_le`, `map_sub_map_piecewise`, `prod_apply`, `curryFinFinset_symm_apply`, `pi_apply`, `Basis.piTensorProduct_repr_tprod_apply`, `congr_arg`, `mk'_apply`, `AlternatingMap.domCoprod_apply`, `exteriorPower.toTensorPower_apply_ιMulti`, `LinearMap.compMultilinearMap_apply`, `snoc_smul`, `PiTensorProduct.tprod_mul_tprod`, `PiTensorProduct.algebraMap_apply`, `coe_injective`, `PiTensorProduct.smul_tprod_mul_smul_tprod`, `TensorPower.toTensorAlgebra_tprod`, `Basis.piTensorProduct_apply`, `PiTensorProduct.congr_tprod`, `map_update_sum`, `PiTensorProduct.map_range_eq_span_tprod`, `zero_apply`, `LinearMap.uncurryLeft_apply`, `ofSubsingleton_apply_apply`, `alternatization_def`, `domDomCongr_apply`, `TensorPower.pairingDual_tprod_tprod`, `coeAddMonoidHom_apply`, `map_add_univ`, `currySum_apply`, `AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero`
`instInhabited` 📖	CompOp	—
`instModule` 📖	CompOp	83 math math: `LinearEquiv.multilinearMapCongrLeft_symm_apply`, `domDomCongrLinearEquiv'_symm_apply`, `PiTensorProduct.lift_reindex`, `LinearEquiv.multilinearMapCongrRight_apply`, `PiTensorProduct.lift.tprod`, `fromDFinsuppEquiv_apply`, `PiTensorProduct.liftAlgHom_apply`, `Module.Finite.multilinearMap`, `PiTensorProduct.lift_reindex_symm`, `currySum_add`, `currySumEquiv_apply`, `PiTensorProduct.toDualContinuousMultilinearMap_apply_apply`, `fromDirectSumEquiv_symm_apply`, `domDomCongrLinearEquiv_symm_apply`, `currySum_apply'`, `PiTensorProduct.reindex_comp_tprod`, `Module.Free.multilinearMap`, `curryFinFinset_apply`, `LinearEquiv.multilinearMapCongrRight_symm_apply`, `coe_currySumEquiv_symm`, `curryFinFinset_symm_apply_piecewise_const`, `fromDFinsuppEquiv_single`, `OrderedFinpartition.compAlongOrderedFinpartitionₗ_apply_apply`, `PiTensorProduct.norm_eval_le_injectiveSeminorm`, `PiTensorProduct.liftEquiv_symm_apply`, `AlternatingMap.curryLeft_apply_toMultilinearMap`, `domDomCongrLinearEquiv_apply`, `freeDFinsuppEquiv_single`, `PiTensorProduct.liftEquiv_apply`, `curryMid_apply_apply`, `freeDFinsuppEquiv_def`, `PiTensorProduct.lift_comp_reindex`, `LinearMap.compMultilinearMapₗ_apply`, `LinearMap.uncurryMid_apply`, `curryFinFinset_apply_const`, `freeFinsuppEquiv_def`, `fromDirectSumEquiv_lof`, `domCoprod'_apply`, `instIsTorsionFree`, `curryLeft_apply`, `Basis.multilinearMap_apply_apply`, `dfinsuppFamilyₗ_apply`, `multilinearCurryLeftEquiv_apply`, `constLinearEquivOfIsEmpty_apply`, `curryFinFinset_symm_apply_const`, `domDomCongrLinearEquiv'_apply`, `freeFinsuppEquiv_apply`, `ofSubsingletonₗ_apply`, `piFamilyₗ_apply`, `fromDirectSumEquiv_apply`, `freeFinsuppEquiv_single`, `freeDFinsuppEquiv_apply`, `curryMidLinearEquiv_apply`, `PiTensorProduct.lift_tprod`, `PiTensorProduct.liftIsometry_apply_apply`, `uncurrySum_add`, `PiTensorProduct.norm_eval_le_projectiveSeminorm`, `PiTensorProduct.lift_comp_map`, `multilinearCurryLeftEquiv_symm_apply`, `piLinearMap_apply_apply_apply`, `coe_currySumEquiv`, `uncurrySum_apply`, `curryMidLinearEquiv_symm_apply`, `Basis.multilinearMap_apply`, `PiTensorProduct.lift.unique'`, `PiTensorProduct.lift_comp_reindex_symm`, `constLinearEquivOfIsEmpty_symm_apply`, `compLinearMapMultilinear_apply`, `currySum_smul`, `curryFinFinset_symm_apply`, `PiTensorProduct.lift.unique`, `ContinuousMultilinearMap.toMultilinearMapLinear_apply`, `LinearEquiv.multilinearMapCongrLeft_apply`, `domCoprodDep'_apply`, `uncurrySum_smul`, `compLinearMapₗ_apply`, `fromDFinsuppEquiv_symm_apply`, `AlternatingMap.toMultilinearMapLM_apply`, `LinearMap.uncurryLeft_apply`, `ofSubsingletonₗ_symm_apply`, `currySumEquiv_symm_apply`, `currySum_apply`, `PiTensorProduct.lift_symm`
`instNeg` 📖	CompOp	2 math math: `AlternatingMap.coe_neg`, `neg_apply`
`instSMul` 📖	CompOp	10 math math: `smul_apply`, `AlternatingMap.coe_smul`, `LinearMap.smul_compMultilinearMap`, `dfinsuppFamily_smul`, `coe_smul`, `LinearMap.compMultilinearMap_smul`, `piFamily_smul`, `currySum_smul`, `ContinuousMultilinearMap.toMultilinearMap_smul`, `uncurrySum_smul`
`instSub` 📖	CompOp	2 math math: `sub_apply`, `AlternatingMap.coe_sub`
`instZero` 📖	CompOp	16 math math: `AlternatingMap.coe_zero`, `LinearMap.zero_compMultilinearMap`, `mkPiRing_zero`, `zero_compLinearMap`, `dfinsuppFamily_single_left_apply`, `ContinuousMultilinearMap.toMultilinearMap_zero`, `piFamily_single_left_apply`, `piFamily_single_left`, `comp_linearEquiv_eq_zero_iff`, `LinearMap.compMultilinearMap_zero`, `dfinsuppFamily_zero`, `AlternatingMap.mk_zero`, `dfinsuppFamily_single_left`, `mkPiRing_eq_zero_iff`, `zero_apply`, `piFamily_zero`
`iteratedFDeriv` 📖	CompOp	—
`iteratedFDerivComponent` 📖	CompOp	—
`linearDeriv` 📖	CompOp	3 math math: `map_add_sub_map_add_sub_linearDeriv`, `map_add_eq_map_add_linearDeriv_add`, `linearDeriv_apply`
`map` 📖	CompOp	1 math math: `map_nonempty`
`mk'` 📖	CompOp	1 math math: `mk'_apply`
`mkPiAlgebra` 📖	CompOp	1 math math: `mkPiAlgebra_apply`
`mkPiAlgebraFin` 📖	CompOp	2 math math: `mkPiAlgebraFin_apply`, `mkPiAlgebraFin_apply_const`
`mkPiRing` 📖	CompOp	6 math math: `mkPiRing_zero`, `mkPiRing_apply_one_eq_self`, `Basis.multilinearMap_apply`, `mkPiRing_apply`, `mkPiRing_eq_zero_iff`, `mkPiRing_eq_iff`
`ofSubsingleton` 📖	CompOp	5 math math: `ofSubsingletonₗ_apply`, `ContinuousMultilinearMap.ofSubsingleton_apply_toMultilinearMap`, `ofSubsingleton_symm_apply_apply`, `ofSubsingletonₗ_symm_apply`, `ofSubsingleton_apply_apply`
`ofSubsingletonₗ` 📖	CompOp	2 math math: `ofSubsingletonₗ_apply`, `ofSubsingletonₗ_symm_apply`
`pi` 📖	CompOp	2 math math: `AlternatingMap.coe_pi`, `pi_apply`
`piLinearMap` 📖	CompOp	1 math math: `piLinearMap_apply_apply_apply`
`piRingEquiv` 📖	CompOp	1 math math: `freeDFinsuppEquiv_def`
`prod` 📖	CompOp	2 math math: `AlternatingMap.coe_prod`, `prod_apply`
`range` 📖	CompOp	—
`restr` 📖	CompOp	1 math math: `restr_norm_le`
`restrictScalars` 📖	CompOp	1 math math: `coe_restrictScalars`
`smulRight` 📖	CompOp	3 math math: `smulRight_apply`, `ContinuousMultilinearMap.smulRight_toMultilinearMap`, `AlternatingMap.coe_smulRight`
`toFun` 📖	CompOp	7 math math: `map_update_add'`, `AlternatingMap.map_eq_zero_of_eq'`, `ContinuousAlternatingMap.map_eq_zero_of_eq'`, `map_update_smul'`, `ContinuousMultilinearMap.cont`, `AlternatingMap.toFun_eq_coe`, `toFun_eq_coe`
`toLinearMap` 📖	CompOp	2 math math: `toLinearMap_apply`, `Module.Basis.det_smul_mk_coord_eq_det_update`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`codRestrict_apply_coe` 📖	mathematical	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `MultilinearMap` `instFunLikeForall`	`Submodule.addCommMonoid` `Submodule.module` `codRestrict`	—	—
`coeAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MultilinearMap` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `Pi.addZeroClass` `AddMonoidHom.instFunLike` `coeAddMonoidHom` `instFunLikeForall`	—	—
`coe_inj` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall`	—	`DFunLike.coe_fn_eq`
`coe_injective` 📖	mathematical	—	`MultilinearMap` `DFunLike.coe` `instFunLikeForall`	—	`DFunLike.coe_injective`
`coe_mk` 📖	mathematical	`Function.update` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`DFunLike.coe` `MultilinearMap` `instFunLikeForall`	—	—
`coe_restrictScalars` 📖	mathematical	`IsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `restrictScalars`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `instSMul` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass`	—	—
`coe_sum` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Finset.sum` `addCommMonoid` `Pi.addCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`compLinearMapMultilinear_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.addCommMonoid` `LinearMap.module` `instDistribMulActionOfSMulCommClass` `instFunLikeForall` `compLinearMapMultilinear` `compLinearMapₗ`	—	`smulCommClass_self`
`compLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `compLinearMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	—
`compLinearMap_assoc` 📖	mathematical	—	`compLinearMap` `LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	—
`compLinearMap_id` 📖	mathematical	—	`compLinearMap` `LinearMap.id`	—	`ext`
`compLinearMap_inj` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`compLinearMap`	—	`compLinearMap_injective`
`compLinearMap_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`MultilinearMap` `compLinearMap`	—	`ext` `Function.surjInv_eq` `ext_iff`
`compLinearMapₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MultilinearMap` `addCommMonoid` `instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `compLinearMapₗ` `compLinearMap`	—	`smulCommClass_self`
`compMultilinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `compMultilinearMap` `Sigma.curry`	—	—
`comp_linearEquiv_eq_zero_iff` 📖	mathematical	—	`compLinearMap` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `instZero`	—	`RingHomInvPair.ids` `zero_compLinearMap` `LinearEquiv.surjective`
`congr_arg` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall`	—	`DFunLike.congr_arg`
`congr_fun` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall`	—	`DFunLike.congr_fun`
`cons_add` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Fin.cons` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Fin.update_cons_zero` `map_update_add`
`cons_smul` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Fin.cons` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Fin.update_cons_zero` `map_update_smul`
`constLinearEquivOfIsEmpty_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `addCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `constLinearEquivOfIsEmpty` `constOfIsEmpty`	—	`RingHomInvPair.ids`
`constLinearEquivOfIsEmpty_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `addCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `constLinearEquivOfIsEmpty` `instFunLikeForall` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids`
`constOfIsEmpty_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `constOfIsEmpty`	—	—
`domDomCongrEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `MultilinearMap` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `domDomCongrEquiv` `domDomCongr`	—	—
`domDomCongrEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `MultilinearMap` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `domDomCongrEquiv` `domDomCongr` `Equiv.symm`	—	—
`domDomCongrLinearEquiv'_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `addCommMonoid` `instModule` `LinearEquiv.instEquivLike` `domDomCongrLinearEquiv'` `instFunLikeForall` `Equiv.piCongrLeft'`	—	`RingHomInvPair.ids`
`domDomCongrLinearEquiv'_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `addCommMonoid` `instModule` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `domDomCongrLinearEquiv'` `instFunLikeForall` `Equiv.piCongrLeft'`	—	`RingHomInvPair.ids`
`domDomCongrLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `addCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `domDomCongrLinearEquiv` `Equiv.toFun` `AddEquiv.toEquiv` `instAdd` `domDomCongrEquiv`	—	`RingHomInvPair.ids`
`domDomCongrLinearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `addCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `domDomCongrLinearEquiv` `Equiv.invFun` `AddEquiv.toEquiv` `instAdd` `domDomCongrEquiv`	—	`RingHomInvPair.ids`
`domDomCongr_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `domDomCongr` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	—
`domDomCongr_eq_iff` 📖	mathematical	—	`domDomCongr`	—	`AddEquiv.apply_eq_iff_eq`
`domDomCongr_mul` 📖	mathematical	—	`domDomCongr` `Equiv.Perm` `Equiv.Perm.instMul`	—	—
`domDomCongr_trans` 📖	mathematical	—	`domDomCongr` `Equiv.trans`	—	—
`domDomRestrict_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `domDomRestrict`	—	—
`domDomRestrict_aux` 📖	mathematical	—	`Function.update`	—	—
`domDomRestrict_aux_right` 📖	mathematical	—	`Function.update`	—	`domDomRestrict_aux`
`ext` 📖	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall`	—	`ext`
`ext_ring` 📖	—	`DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLikeForall` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`ext` `nonempty_fintype` `map_smul_univ` `mul_one`
`ext_ring_iff` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLikeForall` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`ext_ring`
`instIsTorsionFree` 📖	mathematical	—	`Module.IsTorsionFree` `MultilinearMap` `addCommMonoid` `instModule`	—	`Function.Injective.moduleIsTorsionFree` `Pi.instModuleIsTorsionFree` `coe_injective` `coe_smul`
`iteratedFDeriv_aux` 📖	mathematical	—	`Function.update` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Set` `Set.instMembership`	—	`eq_or_ne` `Equiv.apply_symm_apply` `Function.update_self` `Function.update_of_ne` `Equiv.symm_apply_apply`
`linearDeriv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `Pi.module` `LinearMap.instFunLike` `linearDeriv` `Finset.sum` `Finset.univ` `MultilinearMap` `instFunLikeForall` `Function.update`	—	`LinearMap.coe_sum` `Finset.sum_congr` `Finset.sum_apply`
`map_add_eq_map_add_linearDeriv_add` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `AddCommGroup.toAddCommMonoid` `instFunLikeForall` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `Pi.module` `LinearMap.instFunLike` `linearDeriv` `Finset.sum` `Finset` `Finset.filter` `Finset.card` `Finset.univ` `Finset.fintype` `Finset.piecewise` `Finset.decidableMem`	—	`add_comm` `map_add_univ` `Finset.powerset_univ` `Finset.sum_filter_add_sum_filter_not` `Finset.sum_congr` `Finset.filter.congr_simp` `le_iff_lt_or_eq` `Finset.filter_or` `Finset.sum_union` `Finset.pairwise_disjoint_powersetCard` `zero_ne_one` `Finset.powersetCard_zero` `Finset.singleton_injective` `Finset.powersetCard_one` `Finset.sum_singleton` `Finset.piecewise_empty` `Finset.sum_map` `Finset.piecewise_singleton` `linearDeriv_apply`
`map_add_sub_map_add_sub_linearDeriv` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DFunLike.coe` `MultilinearMap` `AddCommGroup.toAddCommMonoid` `instFunLikeForall` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `Pi.module` `LinearMap.instFunLike` `linearDeriv` `Pi.instSub` `Finset.sum` `Finset` `Finset.filter` `Finset.card` `Finset.univ` `Finset.fintype` `Finset.piecewise` `Finset.decidableMem`	—	`map_add_eq_map_add_linearDeriv_add` `add_assoc` `add_sub_add_comm` `sub_self` `zero_add` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `add_sub_cancel_left` `Finset.sum_sub_distrib`
`map_add_univ` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Finset.sum` `Finset` `Finset.univ` `Finset.fintype` `Finset.piecewise` `Finset.decidableMem`	—	`Finset.piecewise_univ` `Finset.sum_congr` `Finset.powerset_univ` `map_piecewise_add`
`map_coord_zero` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`DFunLike.coe` `MultilinearMap` `instFunLikeForall`	—	`smul_zero` `Function.update_eq_self` `map_update_smul` `zero_smul`
`map_insertNth_add` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Fin.insertNth` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Fin.update_insertNth` `map_update_add`
`map_insertNth_smul` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Fin.insertNth` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Fin.update_insertNth` `map_update_smul`
`map_nonempty` 📖	mathematical	—	`Set.Nonempty` `SetLike.coe` `SubMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `SubMulAction.instSetLike` `map`	—	`Submodule.zero_mem`
`map_piecewise_add` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Finset.piecewise` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Finset.decidableMem` `Finset.sum` `Finset` `Finset.powerset`	—	`Finset.induction_on` `Finset.piecewise_empty` `Finset.sum_singleton` `Finset.piecewise_insert` `Function.update_self` `Finset.piecewise_eq_of_notMem` `Function.update_of_ne` `Finset.piecewise_eq_of_mem` `map_update_add` `Finset.sum_powerset_insert` `add_comm` `Finset.sum_congr` `Finset.notMem_of_mem_powerset_of_notMem`
`map_piecewise_smul` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `instFunLikeForall` `Finset.piecewise` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Finset.decidableMem` `Finset.prod` `CommSemiring.toCommMonoid`	—	`Finset.induction_on` `Finset.piecewise_empty` `one_smul` `Function.update_self` `Finset.piecewise_eq_of_notMem` `Function.update_of_ne` `Finset.piecewise_insert` `map_update_smul` `Finset.prod_insert` `SemigroupAction.mul_smul`
`map_piecewise_sub_map_piecewise` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DFunLike.coe` `MultilinearMap` `AddCommGroup.toAddCommMonoid` `instFunLikeForall` `Finset.piecewise` `Finset.decidableMem` `LinearOrder.toDecidableEq` `Finset.sum` `Finset` `Finset.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLT`	—	`Finset.piecewise_idem_right` `map_sub_map_piecewise` `Finset.sum_congr` `congr_arg` `Finset.piecewise_eq_of_mem` `eq_or_ne` `Finset.piecewise_eq_of_notMem`
`map_smul_univ` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `instFunLikeForall` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Finset.prod` `CommSemiring.toCommMonoid` `Finset.univ`	—	`Finset.piecewise_univ` `map_piecewise_smul`
`map_sub_map_piecewise` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DFunLike.coe` `MultilinearMap` `AddCommGroup.toAddCommMonoid` `instFunLikeForall` `Finset.piecewise` `Finset.decidableMem` `LinearOrder.toDecidableEq` `Finset.sum` `Finset` `Finset.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLT`	—	`Finset.induction_on_min` `Finset.piecewise_empty` `Finset.sum_empty` `sub_self` `Finset.piecewise_insert` `map_update` `sub_add` `add_comm` `Finset.sum_insert` `lt_irrefl` `Finset.mem_insert` `Finset.sum_congr` `Function.update_of_ne` `LT.lt.ne` `Finset.piecewise_eq_of_notMem` `LT.lt.not_gt` `Function.update_self` `Finset.piecewise_eq_of_mem`
`map_sum` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Finset.sum` `Finset.univ` `Pi.instFintype`	—	`map_sum_finset`
`map_sum_finset` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Finset.sum` `Fintype.piFinset`	—	`map_sum_finset_aux`
`map_sum_finset_aux` 📖	mathematical	`Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `Finset.card`	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Fintype.piFinset`	—	`Nat.strong_induction_on` `Finset.sum_congr` `map_coord_zero` `Finset.sum_empty` `Finset.card_ne_zero` `le_antisymm` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `Finset.card_le_one_iff` `Fintype.mem_piFinset` `Finset.sum_const` `one_nsmul` `Fintype.card_piFinset` `Finset.prod_congr` `Finset.prod_const_one` `Mathlib.Tactic.Push.not_forall_eq` `Finset.one_lt_card_iff` `Function.update_self` `Function.update_of_ne` `Finset.sdiff_union_self_eq_union` `Finset.sum_union` `Finset.disjoint_right` `Finset.sum_lt_sum` `Nat.instIsOrderedCancelAddMonoid` `Finset.card_le_card` `Finset.mem_univ` `Finset.card_sdiff_of_subset` `Finset.card_singleton` `ne_of_gt` `lt_trans` `Fintype.piFinset_disjoint_of_disjoint` `Finset.Subset.antisymm` `Finset.mem_union_right` `Finset.mem_union_left` `Finset.union_subset` `Fintype.piFinset_subset` `map_update_add`
`map_update` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `AddCommGroup.toAddCommMonoid` `instFunLikeForall` `Function.update` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`map_update_sub` `Function.update_eq_self` `sub_sub_cancel`
`map_update_add` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Function.update` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`map_update_add'`
`map_update_add'` 📖	mathematical	—	`toFun` `Function.update` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`map_update_neg` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `AddCommGroup.toAddCommMonoid` `instFunLikeForall` `Function.update` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`eq_neg_of_add_eq_zero_left` `map_update_add` `neg_add_cancel` `map_coord_zero` `Function.update_self`
`map_update_smul` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Function.update` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`map_update_smul'`
`map_update_smul'` 📖	mathematical	—	`toFun` `Function.update` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`map_update_smul_left` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `instFunLikeForall` `Function.update` `Pi.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Monoid.toNatPow` `Fintype.card`	—	`map_piecewise_smul` `Function.update_smul` `Finset.piecewise_erase_univ` `Function.update_self` `Function.update_idem` `Finset.prod_const` `Finset.card_erase_of_mem`
`map_update_sub` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `AddCommGroup.toAddCommMonoid` `instFunLikeForall` `Function.update` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg` `map_update_add` `map_update_neg`
`map_update_sum` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Function.update` `Finset.sum`	—	`Finset.induction` `map_update_zero` `Finset.sum_insert` `map_update_add`
`map_update_zero` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Function.update` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`map_coord_zero` `Function.update_self`
`map_zero` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Set.exists_mem_of_nonempty` `map_coord_zero`
`mk'_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `mk'`	—	—
`mkPiAlgebraFin_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `instFunLikeForall` `mkPiAlgebraFin` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`mkPiAlgebraFin_apply_const` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `instFunLikeForall` `mkPiAlgebraFin` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`List.ofFn_const` `List.prod_replicate`
`mkPiAlgebra_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `instFunLikeForall` `mkPiAlgebra` `Finset.prod` `CommSemiring.toCommMonoid` `Finset.univ`	—	—
`mkPiRing_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLikeForall` `mkPiRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Finset.prod` `CommSemiring.toCommMonoid` `Finset.univ`	—	—
`mkPiRing_apply_one_eq_self` 📖	mathematical	—	`mkPiRing` `DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLikeForall` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`ext_ring` `Finite.of_fintype` `Finset.prod_const_one` `one_smul`
`mkPiRing_eq_iff` 📖	mathematical	—	`mkPiRing`	—	`Finset.prod_const_one` `one_smul`
`mkPiRing_eq_zero_iff` 📖	mathematical	—	`mkPiRing` `MultilinearMap` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`mkPiRing_zero` `mkPiRing_eq_iff`
`mkPiRing_zero` 📖	mathematical	—	`mkPiRing` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `MultilinearMap` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instZero`	—	`ext_ring` `Finite.of_fintype` `mkPiRing_apply` `smul_zero` `zero_apply`
`mk_coe` 📖	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Function.update` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `AddCommGroup.toAddCommMonoid` `instFunLikeForall` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`ofSubsingleton_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Equiv` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofSubsingleton` `LinearMap.instFunLike`	—	—
`ofSubsingleton_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Equiv` `MultilinearMap` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `ofSubsingleton` `instFunLikeForall`	—	—
`ofSubsingletonₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `MultilinearMap` `LinearMap.addCommMonoid` `addCommMonoid` `LinearMap.module` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `ofSubsingletonₗ` `Equiv` `Equiv.instEquivLike` `ofSubsingleton`	—	`RingHomInvPair.ids`
`ofSubsingletonₗ_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `LinearMap` `addCommMonoid` `LinearMap.addCommMonoid` `instModule` `LinearMap.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `ofSubsingletonₗ` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `ofSubsingleton`	—	`RingHomInvPair.ids`
`piLinearMap_apply_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `instFunLikeForall` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `addCommMonoid` `LinearMap.module` `instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `CommMonoid.toMonoid` `instDistribMulActionOfSMulCommClass` `LinearMap.instFunLike` `piLinearMap`	—	`smulCommClass_self`
`pi_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `Pi.addCommMonoid` `Pi.module` `instFunLikeForall` `pi`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLikeForall` `prod`	—	—
`smulRight_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `instFunLikeForall` `smulRight` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass`	—	—
`snoc_add` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Fin.snoc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Fin.update_snoc_last` `map_update_add`
`snoc_smul` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Fin.snoc` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Fin.update_snoc_last` `map_update_smul`
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `AddCommGroup.toAddCommMonoid` `instFunLikeForall` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`sum_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `Finset.sum` `addCommMonoid`	—	`coe_sum` `Finset.sum_apply`
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `MultilinearMap` `instFunLikeForall`	—	—
`toLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `toLinearMap` `MultilinearMap` `instFunLikeForall` `Function.update`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `instFunLikeForall` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`zero_compLinearMap` 📖	mathematical	—	`compLinearMap` `MultilinearMap` `instZero`	—	`ext`

(root)

Definitions

Name	Category	Theorems
`MultilinearMap` 📖	CompData	282 math math: `MultilinearMap.map_piecewise_smul`, `LinearEquiv.multilinearMapCongrLeft_symm_apply`, `MultilinearMap.domDomCongrLinearEquiv'_symm_apply`, `TensorAlgebra.ofDirectSum_of_tprod`, `PiTensorProduct.lift_reindex`, `AlternatingMap.domCoprod.summand_mk''`, `LinearEquiv.multilinearMapCongrRight_apply`, `PiTensorProduct.lift.tprod`, `MultilinearMap.fromDFinsuppEquiv_apply`, `MultilinearMap.map_update_smul`, `PiTensorProduct.tmulEquiv_symm_apply`, `MultilinearMap.map_update_add`, `PiTensorProduct.isEmptyEquiv_apply_tprod`, `Module.Finite.multilinearMap`, `MultilinearMap.mkPiAlgebra_apply`, `FreeAddMonoid.toPiTensorProduct`, `MultilinearMap.dfinsuppFamily_single`, `PiTensorProduct.ofDirectSumEquiv_tprod_lof`, `MultilinearMap.map_insertNth_add`, `PiTensorProduct.lift_reindex_symm`, `ContinuousMultilinearMap.coe_coe`, `LinearMap.compMultilinearMap_add`, `PiTensorProduct.subsingletonEquiv_symm_apply`, `MultilinearMap.currySum_add`, `TensorAlgebra.toDirectSum_tensorPower_tprod`, `MultilinearMap.piFamily_add`, `MultilinearMap.add_apply`, `ContinuousMultilinearMap.toMultilinearMap_add`, `AlternatingMap.domCoprod_coe`, `MultilinearMap.coe_restrictScalars`, `MultilinearMap.domDomCongrEquiv_symm_apply`, `MultilinearMap.compLinearMap_injective`, `MultilinearMap.smul_apply`, `SemiconjBy.tprod`, `MultilinearMap.congr_fun`, `MultilinearMap.currySumEquiv_apply`, `PiTensorProduct.toDualContinuousMultilinearMap_apply_apply`, `MultilinearMap.map_sum`, `MultilinearMap.map_insertNth_smul`, `MultilinearMap.map_update`, `AlternatingMap.coe_smul`, `MultilinearMap.map_piecewise_sub_map_piecewise`, `MultilinearMap.dfinsuppFamily_apply_toFun`, `MultilinearMap.dfinsuppFamily_apply_support'`, `MultilinearMap.fromDirectSumEquiv_symm_apply`, `MultilinearMap.coe_inj`, `MultilinearMap.curryRight_apply`, `MultilinearMap.domDomCongrLinearEquiv_symm_apply`, `MultilinearMap.currySum_apply'`, `LinearMap.smul_compMultilinearMap`, `PiTensorProduct.reindex_comp_tprod`, `PiTensorProduct.tprod_prod`, `Module.Free.multilinearMap`, `PiTensorProduct.ofFinsuppEquiv'_tprod_single`, `MultilinearMap.curryFinFinset_apply`, `LinearMap.compMultilinearMap_alternatization`, `PiTensorProduct.subsingletonEquiv_apply_tprod`, `MultilinearMap.coe_sum`, `LinearMap.compMultilinearMap_codRestrict`, `PiTensorProduct.projectiveSeminorm_tprod_le`, `PiTensorProduct.ofDirectSumEquiv_symm_lof_tprod`, `PiTensorProduct.tprodL_toFun`, `PiTensorProduct.ofFinsuppEquiv_tprod_single`, `PiTensorProduct.congr_symm_tprod`, `PiTensorProduct.constantBaseRingEquiv_tprod`, `MultilinearMap.domCoprodDep_apply`, `MultilinearMap.dfinsuppFamily_add`, `SymmetricPower.span_tprod_eq_top`, `LinearEquiv.multilinearMapCongrRight_symm_apply`, `MultilinearMap.coe_currySumEquiv_symm`, `MultilinearMap.curryFinFinset_symm_apply_piecewise_const`, `AlternatingMap.coe_zero`, `PiTensorProduct.ofFinsuppEquiv_symm_single_tprod`, `MultilinearMap.domCoprod_alternization_coe`, `PiTensorProduct.one_def`, `MultilinearMap.dfinsuppFamily_smul`, `PiTensorProduct.reindex_tprod`, `LinearMap.zero_compMultilinearMap`, `PiTensorProduct.tprodMonoidHom_apply`, `PiTensorProduct.piTensorHomMap_tprod_tprod`, `MultilinearMap.map_update_smul_left`, `MultilinearMap.fromDFinsuppEquiv_single`, `MultilinearMap.constOfIsEmpty_apply`, `OrderedFinpartition.compAlongOrderedFinpartitionₗ_apply_apply`, `PiTensorProduct.norm_eval_le_injectiveSeminorm`, `MultilinearMap.domCoprod_alternization_eq`, `PiTensorProduct.tprodCoeff_eq_smul_tprod`, `TensorPower.tprod_mul_tprod`, `AlternatingMap.coe_mk`, `PiTensorProduct.liftEquiv_symm_apply`, `MultilinearMap.mkPiRing_zero`, `AlternatingMap.curryLeft_apply_toMultilinearMap`, `MultilinearMap.map_update_neg`, `MultilinearMap.compMultilinearMap_apply`, `MultilinearMap.domDomCongrLinearEquiv_apply`, `MultilinearMap.freeDFinsuppEquiv_single`, `MultilinearMap.map_zero`, `MultilinearMap.map_add_sub_map_add_sub_linearDeriv`, `PiTensorProduct.liftEquiv_apply`, `PiTensorProduct.liftAux_tprodCoeff`, `MultilinearMap.curryMid_apply_apply`, `PiTensorProduct.ofDFinsuppEquiv_tprod_apply`, `MultilinearMap.freeDFinsuppEquiv_def`, `PiTensorProduct.dualDistribInvOfBasis_apply`, `MultilinearMap.coe_mk`, `LinearMap.add_compMultilinearMap`, `MultilinearMap.map_sum_finset_aux`, `PiTensorProduct.piTensorHomMap_tprod_eq_map`, `PiTensorProduct.singleAlgHom_apply`, `PiTensorProduct.lift_comp_reindex`, `TensorPower.multilinearMapToDual_apply_tprod`, `PiTensorProduct.map₂_tprod_tprod`, `LinearMap.compMultilinearMapₗ_apply`, `LinearMap.uncurryMid_apply`, `MultilinearMap.curryFinFinset_apply_const`, `MultilinearMap.freeFinsuppEquiv_def`, `MultilinearMap.map_update_sub`, `LinearMap.coe_compMultilinearMap`, `MultilinearMap.zero_compLinearMap`, `PiTensorProduct.ofFinsuppEquiv_apply`, `MultilinearMap.cons_add`, `MultilinearMap.coe_smul`, `MultilinearMap.fromDirectSumEquiv_lof`, `MultilinearMap.domCoprod'_apply`, `PiTensorProduct.mapMultilinear_apply`, `PiTensorProduct.dualDistrib_apply`, `MultilinearMap.instIsTorsionFree`, `MultilinearMap.curryLeft_apply`, `MultilinearMap.map_update_zero`, `PiTensorProduct.tprod_eq_tprodCoeff_one`, `Basis.multilinearMap_apply_apply`, `MultilinearMap.dfinsuppFamilyₗ_apply`, `PiTensorProduct.isEmptyEquiv_symm_apply`, `PiTensorProduct.subsingletonEquiv_symm_apply'`, `MultilinearMap.map_add_eq_map_add_linearDeriv_add`, `multilinearCurryLeftEquiv_apply`, `PiTensorProduct.tmulEquivDep_symm_apply`, `MultilinearMap.piFamily_apply`, `PiTensorProduct.liftAux_tprod`, `MultilinearMap.constLinearEquivOfIsEmpty_apply`, `MultilinearMap.cons_smul`, `MultilinearMap.curryFinFinset_symm_apply_const`, `PiTensorProduct.piTensorHomMap₂_tprod_tprod_tprod`, `MultilinearMap.dfinsuppFamily_single_left_apply`, `MultilinearMap.domDomCongrLinearEquiv'_apply`, `ContinuousMultilinearMap.toMultilinearMap_zero`, `PiTensorProduct.tmulEquivDep_apply`, `MultilinearMap.freeFinsuppEquiv_apply`, `MultilinearMap.map_piecewise_add`, `MultilinearMap.alternatization_apply`, `MultilinearMap.ofSubsingletonₗ_apply`, `MultilinearMap.piFamilyₗ_apply`, `MultilinearMap.fromDirectSumEquiv_apply`, `MultilinearMap.smulRight_apply`, `PiTensorProduct.mem_lifts_iff`, `PiTensorProduct.ofDFinsuppEquiv_tprod_single`, `MultilinearMap.sub_apply`, `PiTensorProduct.map_tprod`, `MultilinearMap.piFamily_single_left_apply`, `AlternatingMap.coe_alternatization`, `MultilinearMap.domDomRestrict_apply`, `MultilinearMap.mkPiAlgebraFin_apply`, `TensorPower.list_prod_gradedMonoid_mk_single`, `MultilinearMap.freeFinsuppEquiv_single`, `ContinuousMultilinearMap.toMultilinearMap_injective`, `LinearMap.compMultilinearMap_smul`, `PiTensorProduct.one_mul`, `MultilinearMap.piFamily_single_left`, `MultilinearMap.map_coord_zero`, `AlternatingMap.coe_multilinearMap_injective`, `MultilinearMap.mkPiRing_apply_one_eq_self`, `MultilinearMap.ext_ring_iff`, `MultilinearMap.domCoprod_apply`, `PiTensorProduct.tprod_noncommProd`, `MultilinearMap.freeDFinsuppEquiv_apply`, `MultilinearMap.uncurryRight_apply`, `PiTensorProduct.mul_one`, `MultilinearMap.piFamily_smul`, `PiTensorProduct.tmulEquiv_apply`, `MultilinearMap.comp_linearEquiv_eq_zero_iff`, `MultilinearMap.domCoprod_alternization`, `ContinuousMultilinearMap.ofSubsingleton_apply_toMultilinearMap`, `MultilinearMap.curryMidLinearEquiv_apply`, `TensorAlgebra.tprod_apply`, `AlternatingMap.coe_neg`, `TensorPower.cast_tprod`, `PiTensorProduct.mul_tprod_tprod`, `MultilinearMap.ofSubsingleton_symm_apply_apply`, `AlternatingMap.coe_multilinearMap`, `PiTensorProduct.tprodL_apply`, `PiTensorProduct.lift_tprod`, `PiTensorProduct.liftIsometry_apply_apply`, `MultilinearMap.uncurrySum_add`, `ContinuousMultilinearMap.alternatization_apply_toAlternatingMap`, `MultilinearMap.support_dfinsuppFamily_subset`, `AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant`, `TensorPower.gOne_def`, `PiTensorProduct.norm_eval_le_projectiveSeminorm`, `MultilinearMap.snoc_add`, `MultilinearMap.neg_apply`, `MultilinearMap.alternatization_coe`, `PiTensorProduct.lift_comp_map`, `MultilinearMap.ext_iff`, `LinearMap.compMultilinearMap_zero`, `MultilinearMap.map_sum_finset`, `multilinearCurryLeftEquiv_symm_apply`, `MultilinearMap.piLinearMap_apply_apply_apply`, `MultilinearMap.toFun_eq_coe`, `MultilinearMap.coe_currySumEquiv`, `MultilinearMap.uncurrySum_apply`, `MultilinearMap.curryMidLinearEquiv_symm_apply`, `Commute.tprod`, `PiTensorProduct.ofFinsuppEquiv'_apply_apply`, `MultilinearMap.dfinsuppFamily_zero`, `AlternatingMap.coe_add`, `MultilinearMap.piFamily_single`, `Basis.multilinearMap_apply`, `MultilinearMap.compLinearMap_apply`, `PiTensorProduct.lift.unique'`, `SymmetricPower.tprod_equiv`, `MultilinearMap.mkPiAlgebraFin_apply_const`, `AlternatingMap.mk_zero`, `PiTensorProduct.lift_comp_reindex_symm`, `PiTensorProduct.ofDFinsuppEquiv_symm_single_tprod`, `MultilinearMap.linearDeriv_apply`, `PiTensorProduct.span_tprod_eq_top`, `MultilinearMap.mkPiRing_apply`, `MultilinearMap.map_smul_univ`, `MultilinearMap.toLinearMap_apply`, `MultilinearMap.constLinearEquivOfIsEmpty_symm_apply`, `MultilinearMap.compLinearMapMultilinear_apply`, `TensorAlgebra.toDirectSum_ι`, `MultilinearMap.currySum_smul`, `MultilinearMap.sum_apply`, `PiTensorProduct.ofDirectSumEquiv_tprod_apply`, `PiTensorProduct.injectiveSeminorm_tprod_le`, `MultilinearMap.map_sub_map_piecewise`, `MultilinearMap.prod_apply`, `MultilinearMap.curryFinFinset_symm_apply`, `MultilinearMap.pi_apply`, `Basis.piTensorProduct_repr_tprod_apply`, `MultilinearMap.dfinsuppFamily_single_left`, `MultilinearMap.congr_arg`, `MultilinearMap.mk'_apply`, `AlternatingMap.domCoprod_apply`, `MultilinearMap.mkPiRing_eq_zero_iff`, `AlternatingMap.coe_sub`, `exteriorPower.toTensorPower_apply_ιMulti`, `ContinuousMultilinearMap.toMultilinearMap_smul`, `LinearMap.compMultilinearMap_apply`, `MultilinearMap.snoc_smul`, `PiTensorProduct.tprod_mul_tprod`, `PiTensorProduct.algebraMap_apply`, `ContinuousMultilinearMap.toMultilinearMapLinear_apply`, `LinearEquiv.multilinearMapCongrLeft_apply`, `MultilinearMap.domCoprodDep'_apply`, `MultilinearMap.uncurrySum_smul`, `MultilinearMap.coe_injective`, `PiTensorProduct.smul_tprod_mul_smul_tprod`, `TensorPower.toTensorAlgebra_tprod`, `MultilinearMap.compLinearMapₗ_apply`, `MultilinearMap.fromDFinsuppEquiv_symm_apply`, `Basis.piTensorProduct_apply`, `PiTensorProduct.congr_tprod`, `MultilinearMap.map_update_sum`, `PiTensorProduct.map_range_eq_span_tprod`, `AlternatingMap.toMultilinearMapLM_apply`, `MultilinearMap.zero_apply`, `LinearMap.uncurryLeft_apply`, `MultilinearMap.ofSubsingletonₗ_symm_apply`, `MultilinearMap.ofSubsingleton_apply_apply`, `MultilinearMap.alternatization_def`, `MultilinearMap.currySumEquiv_symm_apply`, `MultilinearMap.domDomCongr_apply`, `TensorPower.pairingDual_tprod_tprod`, `MultilinearMap.domDomCongrEquiv_apply`, `MultilinearMap.coeAddMonoidHom_apply`, `MultilinearMap.map_add_univ`, `MultilinearMap.currySum_apply`, `PiTensorProduct.lift_symm`, `AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero`, `MultilinearMap.piFamily_zero`

---

← Back to Index