The Serre class of finite abelian groups

In this file, we define isFinite : ObjectProperty AddCommGrp and show that it is a Serre class.

def AddCommGrp.isFinite : CategoryTheory.ObjectProperty AddCommGrp

The Serre class of finite abelian groups in the category of abelian groups.

Equations

• M.isFinite = Finite ↑M

@[simp]

theorem AddCommGrp.prop_isFinite_iff (M : AddCommGrp) : M.isFinite ↔ Finite ↑M

instance AddCommGrp.instIsSerreClassIsFinite : isFinite.IsSerreClass