Radical

📁 Source: Mathlib/CategoryTheory/Abelian/Preradical/Radical.lean

Statistics

Metric	Count
Definitions isRadical, Radical	2
Theorems isRadical_iff_isIso, isRadical_iff_isZero, instIsIsoPreradicalToColonObjIsRadical, isZero	4
Total	6

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
Radical 📖	CompOp	—

CategoryTheory.Abelian.Preradical

Definitions

Name	Category	Theorems
isRadical 📖	CompOp	4 math math: isRadical_iff_isZero, isRadical_iff_isIso, CategoryTheory.Abelian.Radical.instIsIsoPreradicalToColonObjIsRadical, CategoryTheory.Abelian.Radical.isZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRadical_iff_isIso 📖	mathematical	—	isRadical CategoryTheory.IsIso CategoryTheory.Abelian.Preradical CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.instCategoryOver CategoryTheory.Over.isMono colon toColon	—	—
isRadical_iff_isZero 📖	mathematical	—	isRadical CategoryTheory.Limits.IsZero CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp quotient r	—	isRadical_iff_isIso isIso_toColon_iff

CategoryTheory.Abelian.Radical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoPreradicalToColonObjIsRadical 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Abelian.Preradical CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Abelian.Preradical.isRadical CategoryTheory.Abelian.Preradical.colon CategoryTheory.Abelian.Preradical.toColon	—	CategoryTheory.ObjectProperty.FullSubcategory.property
isZero 📖	mathematical	—	CategoryTheory.Limits.IsZero CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Abelian.Preradical.quotient CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Abelian.Preradical CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.Functor.id CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Abelian.Preradical.isRadical CategoryTheory.Abelian.Preradical.r	—	CategoryTheory.Abelian.Preradical.isRadical_iff_isZero CategoryTheory.Abelian.Preradical.isRadical_iff_isIso instIsIsoPreradicalToColonObjIsRadical

---

← Back to Index