Documentation Verification Report

GroupLike

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

Statistics

Metric	Count
Definitions `instCommMonoid`, `instMonoid`, `instMul`, `instOne`, `instPowNat`, `valMonoidHom`, `groupLikeSubmonoid`	7
Theorems `valMonoidHom_apply`, `val_mul`, `val_one`, `val_pow`, `mul`, `of_mul_eq_one`, `of_unitsInv`, `one`, `pow`, `unitsInv`, `isGroupLikeElem_iff_of_mul_eq_one`, `isGroupLikeElem_unitsInv`	12
Total	19

GroupLike

Definitions

Name	Category	Theorems
`instCommMonoid` 📖	CompOp	—
`instMonoid` 📖	CompOp	3 math math: `valMonoidHom_apply`, `val_toUnits_apply`, `val_inv_toUnits_apply`
`instMul` 📖	CompOp	1 math math: `val_mul`
`instOne` 📖	CompOp	1 math math: `val_one`
`instPowNat` 📖	CompOp	1 math math: `val_pow`
`valMonoidHom` 📖	CompOp	1 math math: `valMonoidHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`valMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `GroupLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike` `valMonoidHom` `val`	—	—
`val_mul` 📖	mathematical	—	`val` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra` `GroupLike` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`val_one` 📖	mathematical	—	`val` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra` `GroupLike` `instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`val_pow` 📖	mathematical	—	`val` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra` `GroupLike` `instPowNat` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—

IsGroupLikeElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul` 📖	mathematical	`IsGroupLikeElem` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Bialgebra.counit_mul` `counit_eq_one` `mul_one` `Algebra.to_smulCommClass` `IsScalarTower.right` `Bialgebra.comul_mul` `comul_eq_tmul_self`
`of_mul_eq_one` 📖	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `IsGroupLikeElem` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra`	—	—	`left_inv_eq_right_inv` `Bialgebra.counit_one` `counit_eq_one` `mul_one` `Algebra.to_smulCommClass` `IsScalarTower.right` `Bialgebra.comul_one` `comul_eq_tmul_self`
`of_unitsInv` 📖	—	`IsGroupLikeElem` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `Units.instInv`	—	—	`isGroupLikeElem_unitsInv`
`one` 📖	mathematical	—	`IsGroupLikeElem` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Bialgebra.counit_one` `Bialgebra.comul_one`
`pow` 📖	mathematical	`IsGroupLikeElem` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Submonoid.pow_mem`
`unitsInv` 📖	mathematical	`IsGroupLikeElem` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Units` `Units.instInv`	—	`isGroupLikeElem_unitsInv`

(root)

Definitions

Name	Category	Theorems
`groupLikeSubmonoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isGroupLikeElem_iff_of_mul_eq_one` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`IsGroupLikeElem` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra`	—	`IsGroupLikeElem.of_mul_eq_one`
`isGroupLikeElem_unitsInv` 📖	mathematical	—	`IsGroupLikeElem` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `Bialgebra.toCoalgebra` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `Units.instInv`	—	`isGroupLikeElem_iff_of_mul_eq_one` `Units.inv_mul` `Units.mul_inv`

---

← Back to Index