Finite

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

Statistics

Metric	Count
Definitions	0
Theorems fg, instFG, instFG, fg	4
Total	4

AddLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg 📖	mathematical	AddSubmonoid.FG AddCommMonoid.toAddMonoid	AddMonoid.FG AddLocalization AddOreLocalization.instAddMonoid AddOreLocalization.addOreSetComm	—	AddMonoid.fg_of_surjective Prod.instAddMonoidFG AddMonoid.fg_iff_addSubmonoid_fg mkHom_surjective

Algebra.GrothendieckAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFG 📖	mathematical	—	AddMonoid.FG Algebra.GrothendieckAddGroup AddOreLocalization.instAddMonoid AddCommMonoid.toAddMonoid Top.top AddSubmonoid AddMonoid.toAddZeroClass AddSubmonoid.instTop AddOreLocalization.addOreSetComm	—	AddLocalization.fg AddMonoid.FG.fg_top

Algebra.GrothendieckGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFG 📖	mathematical	—	Monoid.FG Algebra.GrothendieckGroup OreLocalization.instMonoid CommMonoid.toMonoid Top.top Submonoid Monoid.toMulOneClass Submonoid.instTop OreLocalization.oreSetComm	—	Localization.fg Monoid.FG.fg_top

Localization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg 📖	mathematical	Submonoid.FG CommMonoid.toMonoid	Monoid.FG Localization OreLocalization.instMonoid OreLocalization.oreSetComm	—	Monoid.fg_of_surjective Prod.instMonoidFG Monoid.fg_iff_submonoid_fg mkHom_surjective

---

← Back to Index