MonoidAlgebra

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

Statistics

Metric	Count
Definitions instHopfAlgebra, instHopfAlgebraStruct, instHopfAlgebra, instHopfAlgebra, instHopfAlgebraStruct	5
Theorems antipode_single, antipode_C, antipode_C_mul_T, antipode_T, antipode_single	5
Total	10

AddMonoidAlgebra

Definitions

Name	Category	Theorems
instHopfAlgebra 📖	CompOp	—
instHopfAlgebraStruct 📖	CompOp	4 math math: LaurentPolynomial.antipode_T, LaurentPolynomial.antipode_C, antipode_single, LaurentPolynomial.antipode_C_mul_T

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antipode_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddMonoidAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra instHopfAlgebraStruct LinearMap.instFunLike HopfAlgebraStruct.antipode single NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid HopfAlgebra.toHopfAlgebraStruct	—	Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero

LaurentPolynomial

Definitions

Name	Category	Theorems
instHopfAlgebra 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antipode_C 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LaurentPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.semiring SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra AddMonoidAlgebra.instHopfAlgebraStruct LinearMap.instFunLike HopfAlgebraStruct.antipode RingHom AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C HopfAlgebra.toHopfAlgebraStruct	—	single_eq_C AddMonoidAlgebra.antipode_single neg_zero single_eq_C_mul_T mul_one
antipode_C_mul_T 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LaurentPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.semiring SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra AddMonoidAlgebra.instHopfAlgebraStruct LinearMap.instFunLike HopfAlgebraStruct.antipode AddMonoidAlgebra.instMul RingHom AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T HopfAlgebra.toHopfAlgebraStruct	—	AddMonoidAlgebra.antipode_single
antipode_T 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LaurentPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.semiring SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra AddMonoidAlgebra.instHopfAlgebraStruct LinearMap.instFunLike HopfAlgebraStruct.antipode T	—	AddMonoidAlgebra.antipode_single HopfAlgebra.antipode_one single_eq_C_mul_T map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_mul

MonoidAlgebra

Definitions

Name	Category	Theorems
instHopfAlgebra 📖	CompOp	—
instHopfAlgebraStruct 📖	CompOp	1 math math: antipode_single

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antipode_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MonoidAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring DivInvMonoid.toMonoid Group.toDivInvMonoid Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra instHopfAlgebraStruct LinearMap.instFunLike HopfAlgebraStruct.antipode single InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid HopfAlgebra.toHopfAlgebraStruct	—	Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero

---

← Back to Index