CompTypeclasses

📁 Source: Mathlib/Logic/Function/CompTypeclasses.lean

Statistics

Metric	Count
Definitions CompTriple, IsId	2
Theorems eq_id, comp, comp_apply, comp_eq, comp_inv, instComp_id, instId_comp, instIsIdId	8
Total	10

CompTriple

Definitions

Name	Category	Theorems
IsId 📖	CompData	1 math math: instIsIdId

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	CompTriple	—	—
comp_apply 📖	—	—	—	—	comp_eq
comp_eq 📖	—	—	—	—	—
comp_inv 📖	mathematical	—	CompTriple	—	IsId.eq_id
instComp_id 📖	mathematical	—	CompTriple	—	IsId.eq_id
instId_comp 📖	mathematical	—	CompTriple	—	IsId.eq_id
instIsIdId 📖	mathematical	—	IsId	—	—

CompTriple.IsId

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_id 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
CompTriple 📖	CompData	7 math math: MonoidHom.CompTriple.instRootCompTriple, CompTriple.instId_comp, MulAction.stabilizerEquivStabilizer_compTriple, CompTriple.comp_inv, CompTriple.instComp_id, CompTriple.comp, AddAction.stabilizerEquivStabilizer_compTriple

---

← Back to Index