Basic

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

Statistics

Metric	Count
Definitions toHopfAlgebra, HopfAlgebra, toHopfAlgebraStruct, HopfAlgebraStruct, antipode, toBialgebra	6
Theorems antipode_eq_id, antipode_one, counit_antipode, counit_comp_antipode, mul_antipode_lTensor_comul, mul_antipode_lTensor_comul_apply, mul_antipode_rTensor_comul, mul_antipode_rTensor_comul_apply, sum_antipode_mul_eq_algebraMap_counit, sum_antipode_mul_eq_smul, sum_mul_antipode_eq_algebraMap_counit, sum_mul_antipode_eq_smul	12
Total	18

CommSemiring

Definitions

Name	Category	Theorems
toHopfAlgebra 📖	CompOp	4 math math: HopfAlgCat.rightUnitor_def, antipode_eq_id, HopfAlgCat.leftUnitor_def, HopfAlgCat.tensorUnit_instHopfAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antipode_eq_id 📖	mathematical	—	HopfAlgebraStruct.antipode toSemiring HopfAlgebra.toHopfAlgebraStruct toHopfAlgebra LinearMap.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra	—	—

HopfAlgebra

Definitions

Name	Category	Theorems
toHopfAlgebraStruct 📖	CompOp	48 math math: HopfAlgCat.of_comul, HopfAlgCat.rightUnitor_def, BialgEquiv.toHopfAlgIso_refl, CategoryTheory.Iso.toHopfAlgEquiv_trans, MonoidAlgebra.antipode_single, HopfAlgCat.tensorObj_instRing, HopfAlgCat.whiskerLeft_def, HopfAlgCat.of_counit, HopfAlgCat.tensorObj_instHopfAlgebra, HopfAlgCat.Hom.toBialgHom_injective, HopfAlgCat.forget_reflects_isos, sum_mul_antipode_eq_smul, sum_mul_antipode_eq_algebraMap_counit, HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso, HopfAlgCat.whiskerRight_def, HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso, HopfAlgCat.toBialgHom_comp, HopfAlgCat.associator_def, sum_antipode_mul_eq_smul, HopfAlgCat.forget₂_bialgebra_obj, BialgEquiv.toHopfAlgIso_symm, mul_antipode_rTensor_comul, CategoryTheory.Iso.toHopfAlgEquiv_symm, counit_comp_antipode, mul_antipode_rTensor_comul_apply, GroupLike.val_toUnits_apply, HopfAlgCat.toBialgHom_id, HopfAlgCat.tensorHom_def, GroupLike.val_inv, counit_antipode, CommSemiring.antipode_eq_id, CategoryTheory.Iso.toHopfAlgEquiv_refl, HopfAlgCat.forget₂_bialgebra_map, LaurentPolynomial.antipode_C, GroupLike.val_inv_toUnits_apply, mul_antipode_lTensor_comul_apply, BialgEquiv.toHopfAlgIso_trans, HopfAlgCat.tensorObj_carrier, HopfAlgCat.leftUnitor_def, sum_antipode_mul_eq_algebraMap_counit, mul_antipode_lTensor_comul, AddMonoidAlgebra.antipode_single, TensorProduct.antipode_def, BialgEquiv.toHopfAlgIso_hom, CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom, BialgEquiv.toHopfAlgIso_inv, antipode_one, LaurentPolynomial.antipode_C_mul_T

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antipode_one 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra toHopfAlgebraStruct LinearMap.instFunLike HopfAlgebraStruct.antipode AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Algebra.to_smulCommClass IsScalarTower.right Bialgebra.comul_one mul_one Bialgebra.counit_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_antipode_rTensor_comul_apply
counit_antipode 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra toHopfAlgebraStruct Semiring.toModule LinearMap.instFunLike CoalgebraStruct.counit Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra HopfAlgebraStruct.antipode	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr Bialgebra.counit_mul SemilinearMapClass.toMulActionSemiHomClass Coalgebra.sum_counit_smul map_smul Bialgebra.counit_one mul_one sum_mul_antipode_eq_smul
counit_comp_antipode 📖	mathematical	—	LinearMap.comp CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra toHopfAlgebraStruct Semiring.toModule RingHom.id RingHomCompTriple.ids CoalgebraStruct.counit Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra HopfAlgebraStruct.antipode	—	LinearMap.ext RingHomCompTriple.ids counit_antipode
mul_antipode_lTensor_comul 📖	mathematical	—	LinearMap.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra toHopfAlgebraStruct CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id RingHomCompTriple.ids LinearMap.mul' Algebra.to_smulCommClass IsScalarTower.right LinearMap.lTensor HopfAlgebraStruct.antipode CoalgebraStruct.comul Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra Semiring.toModule Algebra.linearMap CoalgebraStruct.counit	—	—
mul_antipode_lTensor_comul_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra toHopfAlgebraStruct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.mul' Algebra.to_smulCommClass IsScalarTower.right LinearMap.lTensor HopfAlgebraStruct.antipode CoalgebraStruct.comul Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra RingHom RingHom.instFunLike algebraMap Semiring.toModule CoalgebraStruct.counit	—	LinearMap.congr_fun RingHomCompTriple.ids Algebra.to_smulCommClass IsScalarTower.right mul_antipode_lTensor_comul
mul_antipode_rTensor_comul 📖	mathematical	—	LinearMap.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra toHopfAlgebraStruct CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id RingHomCompTriple.ids LinearMap.mul' Algebra.to_smulCommClass IsScalarTower.right LinearMap.rTensor HopfAlgebraStruct.antipode CoalgebraStruct.comul Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra Semiring.toModule Algebra.linearMap CoalgebraStruct.counit	—	—
mul_antipode_rTensor_comul_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra toHopfAlgebraStruct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.mul' Algebra.to_smulCommClass IsScalarTower.right LinearMap.rTensor HopfAlgebraStruct.antipode CoalgebraStruct.comul Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra RingHom RingHom.instFunLike algebraMap Semiring.toModule CoalgebraStruct.counit	—	LinearMap.congr_fun RingHomCompTriple.ids Algebra.to_smulCommClass IsScalarTower.right mul_antipode_rTensor_comul
sum_antipode_mul_eq_algebraMap_counit 📖	mathematical	—	Finset.sum Coalgebra.Repr.ι NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra toHopfAlgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra Coalgebra.Repr.index Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id LinearMap.instFunLike HopfAlgebraStruct.antipode Coalgebra.Repr.left Coalgebra.Repr.right RingHom RingHom.instFunLike algebraMap Semiring.toModule CoalgebraStruct.counit	—	RingHomCompTriple.ids Algebra.to_smulCommClass IsScalarTower.right Coalgebra.Repr.eq map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr mul_antipode_rTensor_comul
sum_antipode_mul_eq_smul 📖	mathematical	—	Finset.sum Coalgebra.Repr.ι NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra toHopfAlgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra Coalgebra.Repr.index Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id LinearMap.instFunLike HopfAlgebraStruct.antipode Coalgebra.Repr.left Coalgebra.Repr.right Algebra.toSMul Semiring.toModule CoalgebraStruct.counit AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	sum_antipode_mul_eq_algebraMap_counit Algebra.smul_def mul_one
sum_mul_antipode_eq_algebraMap_counit 📖	mathematical	—	Finset.sum Coalgebra.Repr.ι NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra toHopfAlgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra Coalgebra.Repr.index Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Coalgebra.Repr.left DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id LinearMap.instFunLike HopfAlgebraStruct.antipode Coalgebra.Repr.right RingHom RingHom.instFunLike algebraMap Semiring.toModule CoalgebraStruct.counit	—	RingHomCompTriple.ids Algebra.to_smulCommClass IsScalarTower.right Coalgebra.Repr.eq map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr mul_antipode_lTensor_comul
sum_mul_antipode_eq_smul 📖	mathematical	—	Finset.sum Coalgebra.Repr.ι NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra toHopfAlgebraStruct Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra Coalgebra.Repr.index Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Coalgebra.Repr.left DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id LinearMap.instFunLike HopfAlgebraStruct.antipode Coalgebra.Repr.right Algebra.toSMul Semiring.toModule CoalgebraStruct.counit AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	sum_mul_antipode_eq_algebraMap_counit Algebra.smul_def mul_one

HopfAlgebraStruct

Definitions

Name	Category	Theorems
antipode 📖	CompOp	24 math math: MonoidAlgebra.antipode_single, IsGroupLikeElem.antipode_antipode, HopfAlgebra.sum_mul_antipode_eq_smul, LaurentPolynomial.antipode_T, HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit, HopfAlgebra.sum_antipode_mul_eq_smul, HopfAlgebra.mul_antipode_rTensor_comul, IsGroupLikeElem.antipode, HopfAlgebra.counit_comp_antipode, HopfAlgebra.mul_antipode_rTensor_comul_apply, IsGroupLikeElem.antipode_mul_cancel, GroupLike.val_inv, HopfAlgebra.counit_antipode, CommSemiring.antipode_eq_id, LaurentPolynomial.antipode_C, GroupLike.val_inv_toUnits_apply, HopfAlgebra.mul_antipode_lTensor_comul_apply, HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit, HopfAlgebra.mul_antipode_lTensor_comul, AddMonoidAlgebra.antipode_single, TensorProduct.antipode_def, IsGroupLikeElem.mul_antipode_cancel, HopfAlgebra.antipode_one, LaurentPolynomial.antipode_C_mul_T
toBialgebra 📖	CompOp	49 math math: HopfAlgCat.of_comul, HopfAlgCat.rightUnitor_def, BialgEquiv.toHopfAlgIso_refl, CategoryTheory.Iso.toHopfAlgEquiv_trans, MonoidAlgebra.antipode_single, HopfAlgCat.tensorObj_instRing, HopfAlgCat.whiskerLeft_def, HopfAlgCat.of_counit, HopfAlgCat.tensorObj_instHopfAlgebra, HopfAlgCat.Hom.toBialgHom_injective, HopfAlgCat.forget_reflects_isos, HopfAlgebra.sum_mul_antipode_eq_smul, LaurentPolynomial.antipode_T, HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit, HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso, HopfAlgCat.whiskerRight_def, HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso, HopfAlgCat.toBialgHom_comp, HopfAlgCat.associator_def, HopfAlgebra.sum_antipode_mul_eq_smul, HopfAlgCat.forget₂_bialgebra_obj, BialgEquiv.toHopfAlgIso_symm, HopfAlgebra.mul_antipode_rTensor_comul, CategoryTheory.Iso.toHopfAlgEquiv_symm, HopfAlgebra.counit_comp_antipode, HopfAlgebra.mul_antipode_rTensor_comul_apply, GroupLike.val_toUnits_apply, HopfAlgCat.toBialgHom_id, HopfAlgCat.tensorHom_def, GroupLike.val_inv, HopfAlgebra.counit_antipode, CommSemiring.antipode_eq_id, CategoryTheory.Iso.toHopfAlgEquiv_refl, HopfAlgCat.forget₂_bialgebra_map, LaurentPolynomial.antipode_C, GroupLike.val_inv_toUnits_apply, HopfAlgebra.mul_antipode_lTensor_comul_apply, BialgEquiv.toHopfAlgIso_trans, HopfAlgCat.tensorObj_carrier, HopfAlgCat.leftUnitor_def, HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit, HopfAlgebra.mul_antipode_lTensor_comul, AddMonoidAlgebra.antipode_single, TensorProduct.antipode_def, BialgEquiv.toHopfAlgIso_hom, CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom, BialgEquiv.toHopfAlgIso_inv, HopfAlgebra.antipode_one, LaurentPolynomial.antipode_C_mul_T

(root)

Definitions

Name	Category	Theorems
HopfAlgebra 📖	CompData	—
HopfAlgebraStruct 📖	CompData	—

---

← Back to Index