Basis

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

Statistics

Metric	Count
Definitions multilinearMap	1
Theorems multilinearMap_apply, multilinearMap_apply_apply, ext_multilinear	3
Total	4

Basis

Definitions

Name	Category	Theorems
multilinearMap 📖	CompOp	2 math math: multilinearMap_apply_apply, multilinearMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multilinearMap_apply 📖	mathematical	Finite	DFunLike.coe Module.Basis MultilinearMap CommSemiring.toSemiring MultilinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Module.Basis.instFunLike multilinearMap Finite.of_fintype LinearMap.compMultilinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule LinearMap.smulRight IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.id MultilinearMap.compLinearMap MultilinearMap.mkPiRing AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Module.Basis.coord	—	MultilinearMap.ext smulCommClass_self Finite.of_fintype IsScalarTower.left RingHomInvPair.ids LinearEquiv.trans.congr_simp Finsupp.smulCommClass Algebra.to_smulCommClass Fintype.subsingleton Module.Basis.coe_repr_symm MultilinearMap.freeFinsuppEquiv_single one_smul Finsupp.linearCombination_single mul_one
multilinearMap_apply_apply 📖	mathematical	Finite	DFunLike.coe MultilinearMap CommSemiring.toSemiring MultilinearMap.instFunLikeForall Module.Basis MultilinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Module.Basis.instFunLike multilinearMap Finite.of_fintype SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finset.prod Finset.univ Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr	—	smulCommClass_self Finite.of_fintype RingHomInvPair.ids IsScalarTower.left multilinearMap_apply mul_one

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_multilinear 📖	—	DFunLike.coe MultilinearMap CommSemiring.toSemiring MultilinearMap.instFunLikeForall Module.Basis instFunLike	—	—	nonempty_fintype MultilinearMap.ext RingHomInvPair.ids Function.Surjective.piMap LinearEquiv.surjective repr_symm_apply Finset.sum_congr MultilinearMap.map_sum_finset MultilinearMap.map_smul_univ

---

← Back to Index