Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-28 19:37 2401d996

View on Github →

feat(group_theory/finiteness): add group.fg (#7338) Basic facts about finitely generated groups.

Estimated changes

added theorem set.finite.inv
added theorem add_group.fg_def
added theorem group.fg_def
added theorem group.fg_iff
added theorem group.fg_iff_monoid.fg
added theorem group_fg.iff_add_fg
added def subgroup.fg
added theorem subgroup.fg_iff
added theorem subgroup.fg_iff_add_fg
modified theorem module.finite_def