Free

📁 Source: Mathlib/LinearAlgebra/TensorProduct/Free.lean

Statistics

Metric	Count
Definitions equivFinsuppOfBasis, equivPiOfFiniteBasis	2
Theorems equivFinsuppOfBasis_apply, equivFinsuppOfBasis_symm_apply, equivPiOfFiniteBasis_apply, equivPiOfFiniteBasis_symm_apply	4
Total	6

Algebra.TensorProduct

Definitions

Name	Category	Theorems
equivFinsuppOfBasis 📖	CompOp	2 math math: equivFinsuppOfBasis_apply, equivFinsuppOfBasis_symm_apply
equivPiOfFiniteBasis 📖	CompOp	2 math math: equivPiOfFiniteBasis_symm_apply, equivPiOfFiniteBasis_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivFinsuppOfBasis_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Algebra.toModule Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Finsupp.module EquivLike.toFunLike LinearEquiv.instEquivLike equivFinsuppOfBasis TensorProduct.finsuppScalarRight LinearMap LinearMap.instFunLike LinearMap.baseChange LinearEquiv.toLinearMap Module.Basis.repr	—	RingHomInvPair.ids Algebra.to_smulCommClass
equivFinsuppOfBasis_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Algebra.toModule Finsupp.instAddCommMonoid TensorProduct.addCommMonoid Finsupp.module Semiring.toModule TensorProduct.leftModule Algebra.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm equivFinsuppOfBasis LinearEquiv.baseChange Module.Basis.repr TensorProduct.finsuppScalarRight	—	RingHomInvPair.ids Algebra.to_smulCommClass
equivPiOfFiniteBasis_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Algebra.toModule TensorProduct.addCommMonoid Pi.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Pi.Function.module EquivLike.toFunLike LinearEquiv.instEquivLike equivPiOfFiniteBasis LinearMap IsScalarTower.to_smulCommClass LinearMap.instFunLike TensorProduct.piScalarRightHom LinearMap.baseChange LinearEquiv.toLinearMap Module.Basis.equivFun	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass TensorProduct.piScalarRight_apply
equivPiOfFiniteBasis_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Algebra.toModule Pi.addCommMonoid TensorProduct.addCommMonoid Pi.Function.module Semiring.toModule TensorProduct.leftModule Algebra.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm equivPiOfFiniteBasis LinearEquiv.baseChange Module.Basis.equivFun TensorProduct.piScalarRight Fintype.ofFinite	—	RingHomInvPair.ids Algebra.to_smulCommClass

---

← Back to Index