Subalgebra.fg_top

theorem Subalgebra.fg_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A), ⊤.FG ↔ S.FG

This theorem states that for any commutative semiring `R`, semiring `A`, and a subalgebra `S` of `A` over `R`, the whole algebra (denoted by `⊤`) being finitely generated is equivalent to the subalgebra `S` being finitely generated. In other words, the property of "being finitely generated" for the whole algebra is the same as for any of its subalgebras.

More concisely: For any commutative semirings `R`, semirings `A`, and a subalgebra `S` of `A` over `R`, the whole algebra `⊤` and subalgebra `S` are finitely generated if and only if each other is.