Documentation Verification Report

GroupLike

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

Statistics

Metric	Count
Definitions `instCoeOut`, `val`, `valEquiv`, `IsGroupLikeElem`	4
Theorems `ext`, `ext_iff`, `isGroupLikeElem_val`, `val_inj`, `val_injective`, `comul_eq_tmul_self`, `counit_eq_one`, `map`, `ne_zero`, `isGroupLikeElem_iff`, `isGroupLikeElem_map_equiv`, `isGroupLikeElem_self`, `linearIndepOn_isGroupLikeElem`, `linearIndep_groupLikeVal`	14
Total	18

GroupLike

Definitions

Name	Category	Theorems
`instCoeOut` 📖	CompOp	—
`val` 📖	CompOp	12 math math: `val_injective`, `linearIndep_groupLikeVal`, `valMonoidHom_apply`, `val_one`, `ext_iff`, `val_mul`, `isGroupLikeElem_val`, `val_toUnits_apply`, `val_inj`, `val_inv`, `val_inv_toUnits_apply`, `val_pow`
`valEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`isGroupLikeElem_val` 📖	mathematical	—	`IsGroupLikeElem` `val`	—	—
`val_inj` 📖	mathematical	—	`val`	—	`val_injective`
`val_injective` 📖	mathematical	—	`GroupLike` `val`	—	`isGroupLikeElem_val`

IsGroupLikeElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comul_eq_tmul_self` 📖	mathematical	`IsGroupLikeElem`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `CoalgebraStruct.comul` `Coalgebra.toCoalgebraStruct` `TensorProduct.tmul`	—	—
`counit_eq_one` 📖	mathematical	`IsGroupLikeElem`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `CoalgebraStruct.counit` `Coalgebra.toCoalgebraStruct` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`map` 📖	mathematical	`IsGroupLikeElem`	`DFunLike.coe`	—	`CoalgHomClass.counit_comp_apply` `counit_eq_one` `CoalgHomClass.toSemilinearMapClass` `CoalgHomClass.map_comp_comul_apply` `comul_eq_tmul_self`
`ne_zero` 📖	—	`IsGroupLikeElem`	—	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `NeZero.one` `counit_eq_one`

(root)

Definitions

Name	Category	Theorems
`IsGroupLikeElem` 📖	CompData	8 math math: `isGroupLikeElem_iff`, `GroupLike.isGroupLikeElem_val`, `isGroupLikeElem_unitsInv`, `isGroupLikeElem_map_equiv`, `isGroupLikeElem_self`, `IsGroupLikeElem.one`, `linearIndepOn_isGroupLikeElem`, `isGroupLikeElem_iff_of_mul_eq_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isGroupLikeElem_iff` 📖	mathematical	—	`IsGroupLikeElem` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `CoalgebraStruct.counit` `Coalgebra.toCoalgebraStruct` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `CoalgebraStruct.comul` `TensorProduct.tmul`	—	—
`isGroupLikeElem_map_equiv` 📖	mathematical	—	`IsGroupLikeElem` `DFunLike.coe` `EquivLike.toFunLike`	—	`IsGroupLikeElem.map` `CoalgEquivClass.toCoalgHomClass` `CoalgEquiv.instCoalgEquivClass` `CoalgEquiv.symm_apply_apply`
`isGroupLikeElem_self` 📖	mathematical	—	`IsGroupLikeElem` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `CommSemiring.toCoalgebra` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`linearIndepOn_isGroupLikeElem` 📖	mathematical	—	`LinearIndepOn` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `setOf` `IsGroupLikeElem`	—	`linearIndepOn_iff_linearIndepOn_finset` `Finset.cons_induction` `Finset.coe_empty` `Finset.cons_eq_insert` `Finset.coe_insert` `Finset.coe_cons` `LinearIndepOn.id_insert'` `LinearIndepOn.tmul_of_isDomain` `Finset.sum_congr` `ite_smul` `SemigroupAction.mul_smul` `zero_smul` `Finset.sum_ite_eq` `Finset.sum_ite_mem` `Finset.inter_self` `Finset.smul_sum` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `IsGroupLikeElem.comul_eq_tmul_self` `smulCommClass_self` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left` `TensorProduct.smul_tmul` `TensorProduct.sum_tmul` `TensorProduct.tmul_sum` `IsDomain.to_noZeroDivisors` `mul_left_injective₀` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Finset.sum_eq_single` `instIsEmptyFalse` `Finset.sum_const_zero` `IsGroupLikeElem.ne_zero` `IsDomain.toNontrivial`
`linearIndep_groupLikeVal` 📖	mathematical	—	`LinearIndependent` `GroupLike` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `GroupLike.val` `CommSemiring.toSemiring`	—	`linearIndependent_equiv` `linearIndepOn_isGroupLikeElem`

---

← Back to Index