TensorProduct

📁 Source: Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean

Statistics

Metric	Count
Definitions ofAlgHom, instHopfAlgebra	2
Theorems antipode_def	1
Total	3

HopfAlgebra

Definitions

Name	Category	Theorems
ofAlgHom 📖	CompOp	—

TensorProduct

Definitions

Name	Category	Theorems
instHopfAlgebra 📖	CompOp	8 math math: HopfAlgCat.rightUnitor_def, HopfAlgCat.whiskerLeft_def, HopfAlgCat.tensorObj_instHopfAlgebra, HopfAlgCat.whiskerRight_def, HopfAlgCat.associator_def, HopfAlgCat.tensorHom_def, HopfAlgCat.leftUnitor_def, antipode_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antipode_def 📖	mathematical	—	HopfAlgebraStruct.antipode TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra HopfAlgebra.toHopfAlgebraStruct Algebra.TensorProduct.instSemiring instHopfAlgebra AlgebraTensorModule.map CommSemiring.toSemiring	—	—

---

← Back to Index