Commit 2023-05-16 06:36 000e226b

View on Github →

refactor: rename Fg to FG (#3948) Please refer to this Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20convention/near/357712556

Estimated changes

modified theorem AddGroup.fg_def
modified theorem AddGroup.fg_iff_mul_fg
modified theorem AddMonoid.fg_def
modified theorem AddMonoid.fg_iff_mul_fg
modified theorem AddSubgroup.fg_iff_mul_fg
modified theorem AddSubmonoid.fg_iff_mul_fg
modified theorem Group.fg_def
modified theorem Group.fg_iff
modified theorem Group.fg_iff_monoid_fg
modified theorem Group.fg_of_surjective
modified theorem Group.rank_congr
modified theorem Group.rank_le
modified theorem Group.rank_le_of_surjective
modified theorem Group.rank_range_le
modified theorem Group.rank_spec
added theorem GroupFG.iff_add_fg
deleted theorem GroupFg.iff_add_fg
modified theorem Monoid.fg_def
modified theorem Monoid.fg_iff_add_fg
modified theorem Monoid.fg_iff_submonoid_fg
modified theorem Monoid.fg_of_surjective
added def Subgroup.FG
deleted def Subgroup.Fg
modified theorem Subgroup.fg_iff_add_fg
modified theorem Subgroup.rank_congr
added theorem Submonoid.FG.map
added def Submonoid.FG
deleted theorem Submonoid.Fg.map
deleted def Submonoid.Fg
modified theorem Submonoid.fg_iff_add_fg
modified theorem Submonoid.powers_fg
modified theorem Algebra.fg_trans
added theorem Subalgebra.FG.map
added theorem Subalgebra.FG.prod
added def Subalgebra.FG
deleted theorem Subalgebra.Fg.map
deleted theorem Subalgebra.Fg.prod
deleted def Subalgebra.Fg
modified theorem Subalgebra.fg_adjoin_finset
modified theorem Subalgebra.fg_bot
modified theorem Subalgebra.fg_def
modified theorem Subalgebra.fg_of_noetherian
modified theorem Subalgebra.fg_top
modified theorem isNoetherianRing_of_fg
modified theorem exists_subalgebra_of_fg
modified theorem fg_of_fg_of_fg
added theorem Ideal.FG.map
added def Ideal.FG
deleted theorem Ideal.Fg.map
deleted def Ideal.Fg
added theorem Submodule.FG.map
added theorem Submodule.FG.map₂
added theorem Submodule.FG.mul
added theorem Submodule.FG.pow
added theorem Submodule.FG.prod
added theorem Submodule.FG.sup
added def Submodule.FG
deleted theorem Submodule.Fg.map
deleted theorem Submodule.Fg.map₂
deleted theorem Submodule.Fg.mul
deleted theorem Submodule.Fg.pow
deleted theorem Submodule.Fg.prod
deleted theorem Submodule.Fg.sup
deleted def Submodule.Fg
modified theorem Submodule.fg_biSup
modified theorem Submodule.fg_bot
modified theorem Submodule.fg_def
modified theorem Submodule.fg_finset_sup
modified theorem Submodule.fg_iSup
modified theorem Submodule.fg_iff_compact
modified theorem Submodule.fg_of_linearEquiv
modified theorem Submodule.fg_span
modified theorem Submodule.fg_span_singleton
modified theorem Submodule.fg_top
modified theorem isNoetherian_def
modified theorem reesAlgebra.fg