GroupLike

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

Statistics

Metric	Count
Definitions GroupLike, instCommGroup, instGroup, instInv, toUnits	5
Theorems val_inv, val_inv_toUnits_apply, val_toUnits_apply, antipode, antipode_antipode, antipode_mul_cancel, isUnit, mul_antipode_cancel	8
Total	13

GroupLike

Definitions

Name	Category	Theorems
instCommGroup 📖	CompOp	—
instGroup 📖	CompOp	—
instInv 📖	CompOp	1 math math: val_inv
toUnits 📖	CompOp	2 math math: val_toUnits_apply, val_inv_toUnits_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
val_inv 📖	mathematical	—	val NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra HopfAlgebra.toHopfAlgebraStruct Bialgebra.toCoalgebra GroupLike instInv DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id LinearMap.instFunLike HopfAlgebraStruct.antipode	—	—
val_inv_toUnits_apply 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units Units.instInv DFunLike.coe MonoidHom GroupLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra HopfAlgebra.toHopfAlgebraStruct Bialgebra.toCoalgebra MulOneClass.toMulOne Monoid.toMulOneClass instMonoid Units.instMulOneClass MonoidHom.instFunLike toUnits LinearMap CommSemiring.toSemiring RingHom.id LinearMap.instFunLike HopfAlgebraStruct.antipode val	—	—
val_toUnits_apply 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom GroupLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra HopfAlgebra.toHopfAlgebraStruct Bialgebra.toCoalgebra Units MulOneClass.toMulOne Monoid.toMulOneClass instMonoid Units.instMulOneClass MonoidHom.instFunLike toUnits val	—	—

IsGroupLikeElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antipode 📖	mathematical	IsGroupLikeElem NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra HopfAlgebra.toHopfAlgebraStruct Bialgebra.toCoalgebra	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id LinearMap.instFunLike HopfAlgebraStruct.antipode	—	of_mul_eq_one mul_antipode_cancel antipode_mul_cancel
antipode_antipode 📖	mathematical	IsGroupLikeElem NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra HopfAlgebra.toHopfAlgebraStruct Bialgebra.toCoalgebra	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id LinearMap.instFunLike HopfAlgebraStruct.antipode	—	left_inv_eq_right_inv antipode_mul_cancel antipode
antipode_mul_cancel 📖	mathematical	IsGroupLikeElem NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra HopfAlgebra.toHopfAlgebraStruct Bialgebra.toCoalgebra	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id LinearMap.instFunLike HopfAlgebraStruct.antipode AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Algebra.to_smulCommClass IsScalarTower.right comul_eq_tmul_self counit_eq_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass HopfAlgebra.mul_antipode_rTensor_comul_apply
isUnit 📖	mathematical	IsGroupLikeElem NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra HopfAlgebra.toHopfAlgebraStruct Bialgebra.toCoalgebra	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Units.isUnit
mul_antipode_cancel 📖	mathematical	IsGroupLikeElem NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toAlgebra HopfAlgebraStruct.toBialgebra HopfAlgebra.toHopfAlgebraStruct Bialgebra.toCoalgebra	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id LinearMap.instFunLike HopfAlgebraStruct.antipode AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Algebra.to_smulCommClass IsScalarTower.right comul_eq_tmul_self counit_eq_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass HopfAlgebra.mul_antipode_lTensor_comul_apply

(root)

Definitions

Name	Category	Theorems
GroupLike 📖	CompData	9 math math: GroupLike.val_injective, linearIndep_groupLikeVal, GroupLike.valMonoidHom_apply, GroupLike.val_one, GroupLike.val_mul, GroupLike.val_toUnits_apply, GroupLike.val_inv, GroupLike.val_inv_toUnits_apply, GroupLike.val_pow

---

← Back to Index