Tensor

📁 Source: Mathlib/Algebra/Module/Presentation/Tensor.lean

Statistics

Metric	Count
Definitions tensor, isPresentationCoreTensor, tensor, tensor	4
Theorems tensor_G, tensor_R, tensor_relation, tensor_var, tensor, tensor_var, tensor_G, tensor_R, tensor_relation	9
Total	13

Module.Presentation

Definitions

Name	Category	Theorems
tensor 📖	CompOp	4 math math: tensor_R, tensor_G, tensor_relation, tensor_var

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensor_G 📖	mathematical	—	Module.Relations.G CommRing.toRing toRelations TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule tensor	—	—
tensor_R 📖	mathematical	—	Module.Relations.R CommRing.toRing toRelations TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule tensor Module.Relations.G	—	—
tensor_relation 📖	mathematical	—	Module.Relations.relation CommRing.toRing toRelations TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule tensor Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.embDomain Function.Embedding.sectL Function.Embedding.sectR	—	—
tensor_var 📖	mathematical	—	Module.Relations.Solution.var CommRing.toRing toRelations TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule tensor toSolution TensorProduct.tmul	—	—

Module.Relations

Definitions

Name	Category	Theorems
tensor 📖	CompOp	5 math math: Solution.IsPresentation.tensor, tensor_R, Solution.tensor_var, tensor_G, tensor_relation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensor_G 📖	mathematical	—	G CommRing.toRing tensor	—	—
tensor_R 📖	mathematical	—	R CommRing.toRing tensor G	—	—
tensor_relation 📖	mathematical	—	relation CommRing.toRing tensor Finsupp G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.embDomain Function.Embedding.sectL Function.Embedding.sectR	—	—

Module.Relations.Solution

Definitions

Name	Category	Theorems
isPresentationCoreTensor 📖	CompOp	—
tensor 📖	CompOp	2 math math: IsPresentation.tensor, tensor_var

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensor_var 📖	mathematical	—	var CommRing.toRing Module.Relations.tensor TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule tensor TensorProduct.tmul	—	—

Module.Relations.Solution.IsPresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensor 📖	mathematical	Module.Relations.Solution.IsPresentation CommRing.toRing	Module.Relations.tensor TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule Module.Relations.Solution.tensor	—	Module.Relations.Solution.IsPresentationCore.isPresentation

---

← Back to Index