Commit 2025-02-27 12:10 9fa74e29

View on Github →

feat: the Serre class of finite abelian groups (#22317)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/Grp/IsFinite.lean

added def AddCommGrp.isFinite

added theorem AddCommGrp.prop_isFinite_iff