EckmannHilton

📁 Source: Mathlib/GroupTheory/EckmannHilton.lean

Statistics

Metric	Count
Definitions IsUnital, addCommGroup, addCommMonoid, commGroup, commMonoid	5
Theorems IsUnital, toLawfulIdentity, isUnital, mul, mul_assoc, mul_comm, one	7
Total	12

EckmannHilton

Definitions

Name	Category	Theorems
IsUnital 📖	CompData	5 math math: HomotopyGroup.isUnital_auxGroup, CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_leftAdd, AddZeroClass.IsUnital, MulOneClass.isUnital, CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_rightAdd
addCommGroup 📖	CompOp	—
addCommMonoid 📖	CompOp	—
commGroup 📖	CompOp	—
commMonoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul 📖	—	IsUnital	—	—	one IsUnital.toLawfulIdentity
mul_assoc 📖	—	IsUnital	—	—	mul IsUnital.toLawfulIdentity
mul_comm 📖	—	IsUnital	—	—	mul IsUnital.toLawfulIdentity
one 📖	—	IsUnital	—	—	IsUnital.toLawfulIdentity

EckmannHilton.AddZeroClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsUnital 📖	mathematical	—	EckmannHilton.IsUnital AddZero.toAdd AddZeroClass.toAddZero AddZero.toZero	—	AddZeroClass.zero_add AddZeroClass.add_zero

EckmannHilton.IsUnital

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLawfulIdentity 📖	—	EckmannHilton.IsUnital	—	—	—

EckmannHilton.MulOneClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnital 📖	mathematical	—	EckmannHilton.IsUnital MulOne.toMul MulOneClass.toMulOne MulOne.toOne	—	MulOneClass.one_mul MulOneClass.mul_one

---

← Back to Index