Finite

📁 Source: Mathlib/GroupTheory/QuotientGroup/Finite.lean

Statistics

Metric	Count
Definitions fintypeOfDomOfCoker, fintypeOfKerEqRange, fintypeOfKerLeRange, fintypeOfKerOfCodom, fintypeOfDomOfCoker, fintypeOfKerEqRange, fintypeOfKerLeRange, fintypeOfKerOfCodom	8
Theorems of_addSubgroup_quotient, of_finite_quot_finite_addSubgroup, of_finite_quot_finite_subgroup, of_subgroup_quotient, finite_iff_addSubgroup_quotient, finite_iff_subgroup_quotient	6
Total	14

AddGroup

Definitions

Name	Category	Theorems
fintypeOfDomOfCoker 📖	CompOp	—
fintypeOfKerEqRange 📖	CompOp	—
fintypeOfKerLeRange 📖	CompOp	—
fintypeOfKerOfCodom 📖	CompOp	—

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_addSubgroup_quotient 📖	mathematical	—	Finite	—	finite_iff_addSubgroup_quotient
of_finite_quot_finite_addSubgroup 📖	mathematical	—	Finite	—	of_addSubgroup_quotient
of_finite_quot_finite_subgroup 📖	mathematical	—	Finite	—	of_subgroup_quotient
of_subgroup_quotient 📖	mathematical	—	Finite	—	finite_iff_subgroup_quotient

Group

Definitions

Name	Category	Theorems
fintypeOfDomOfCoker 📖	CompOp	—
fintypeOfKerEqRange 📖	CompOp	—
fintypeOfKerLeRange 📖	CompOp	—
fintypeOfKerOfCodom 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_iff_addSubgroup_quotient 📖	mathematical	—	Finite AddSubgroup SetLike.instMembership AddSubgroup.instSetLike HasQuotient.Quotient QuotientAddGroup.instHasQuotientAddSubgroup	—	Equiv.finite_iff Prod.finite_iff Zero.instNonempty
finite_iff_subgroup_quotient 📖	mathematical	—	Finite Subgroup SetLike.instMembership Subgroup.instSetLike HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup	—	Equiv.finite_iff Prod.finite_iff One.instNonempty

---

← Back to Index