Graded rings of finite type

We show that graded rings of finite type (over the 0-th component) are generated by homogeneous elements of positive degree.

theorem GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous {S : Type u_1} {σ : Type u_2} {ι : Type u_3} [DecidableEq ι] [AddCommMonoid ι] [CommRing S] [SetLike σ S] [AddSubgroupClass σ S] (𝒜 : ι → σ) [GradedRing 𝒜] [Algebra.FiniteType (↥(𝒜 0)) S] : ∃ (s : Finset S), Algebra.adjoin ↥(𝒜 0) ↑s = ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i

theorem GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero {S : Type u_1} {σ : Type u_2} {ι : Type u_3} [DecidableEq ι] [AddCommMonoid ι] [CommRing S] [SetLike σ S] [AddSubgroupClass σ S] (𝒜 : ι → σ) [GradedRing 𝒜] [Algebra.FiniteType (↥(𝒜 0)) S] : ∃ (s : Finset S), Algebra.adjoin ↥(𝒜 0) ↑s = ⊤ ∧ ∀ i ∈ s, ∃ (n : ι), n ≠ 0 ∧ i ∈ 𝒜 n