Subalgebras that are finitely generated as submodules

theorem Subalgebra.fg_bot_toSubmodule {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : (toSubmodule ⊥).FG

instance Subalgebra.finite_bot {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : Module.Finite R ↥⊥

theorem Submodule.fg_unit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (I : (Submodule R A)ˣ) : (↑I).FG

theorem Submodule.fg_of_isUnit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {I : Submodule R A} (hI : IsUnit I) : I.FG

theorem Submodule.FG.mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {M N : Submodule R A} (hm : M.FG) (hn : N.FG) : (M * N).FG

theorem Submodule.FG.pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {M : Submodule R A} (h : M.FG) (n : ℕ) : (M ^ n).FG