Commit 2023-03-31 10:28 3ba9781d

View on Github →

feat: port RingTheory.Adjoin.Fg (#3199)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Adjoin/Fg.lean

added theorem Algebra.fg_trans

added theorem Subalgebra.Fg.map

added theorem Subalgebra.Fg.prod

added def Subalgebra.Fg

added theorem Subalgebra.fg_adjoin_finset

added theorem Subalgebra.fg_bot

added theorem Subalgebra.fg_def

added theorem Subalgebra.fg_of_fg_map

added theorem Subalgebra.fg_of_fg_toSubmodule

added theorem Subalgebra.fg_of_noetherian

added theorem Subalgebra.fg_of_submodule_fg

added theorem Subalgebra.fg_top

added theorem Subalgebra.induction_on_adjoin

added theorem isNoetherianRing_of_fg

added theorem is_noetherian_subring_closure