ConjFinite

📁 Source: Mathlib/Algebra/Group/ConjFinite.lean

Statistics

Metric	Count
Definitions instFintypeElemCarrier, fintype, instDecidableRelIsConjOfDecidableEqOfFintype, instFintypeConjClassesOfDecidableRelIsConj	4
Theorems instFiniteConjClasses	1
Total	5

ConjClasses

Definitions

Name	Category	Theorems
instFintypeElemCarrier 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
instDecidableRelIsConjOfDecidableEqOfFintype 📖	CompOp	—
instFintypeConjClassesOfDecidableRelIsConj 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteConjClasses 📖	mathematical	—	Finite ConjClasses	—	Quotient.finite

conjugatesOf

Definitions

Name	Category	Theorems
fintype 📖	CompOp	—

---

← Back to Index