Commit 2023-02-11 15:55 a4297454

View on Github →

feat Port/GroupTheory.Finiteness (#2187)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Finiteness.lean

added theorem AddGroup.fg_def

added theorem AddGroup.fg_iff_mul_fg

added theorem AddMonoid.fg_def

added theorem AddMonoid.fg_iff_mul_fg

added theorem AddSubgroup.fg_iff_mul_fg

added theorem AddSubmonoid.fg_iff_mul_fg

added theorem Group.FgIffMonoid.fg

added theorem Group.fg_def

added theorem Group.fg_iff'

added theorem Group.fg_iff

added theorem Group.fg_of_surjective

added theorem Group.rank_congr

added theorem Group.rank_le

added theorem Group.rank_le_of_surjective

added theorem Group.rank_range_le

added theorem Group.rank_spec

added theorem GroupFg.iff_add_fg

added theorem Monoid.fg_def

added theorem Monoid.fg_iff

added theorem Monoid.fg_iff_add_fg

added theorem Monoid.fg_iff_submonoid_fg

added theorem Monoid.fg_of_surjective

added def Subgroup.Fg

added theorem Subgroup.fg_iff

added theorem Subgroup.fg_iff_add_fg

added theorem Subgroup.fg_iff_submonoid_fg

added theorem Subgroup.rank_closure_finite_le_nat_card

added theorem Subgroup.rank_closure_finset_le_card

added theorem Subgroup.rank_congr

added theorem Submonoid.Fg.map

added theorem Submonoid.Fg.map_injective

added def Submonoid.Fg

added theorem Submonoid.fg_iff

added theorem Submonoid.fg_iff_add_fg

added theorem Submonoid.powers_fg