theorem SetLike.Homogeneous.exists_homogeneous_of_dvd {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] {a c : A} (hom_a : SetLike.Homogeneous 𝒜 a) (hom_c : SetLike.Homogeneous 𝒜 c) (dvd : a ∣ c) : ∃ (b : A), a * b = c ∧ SetLike.Homogeneous 𝒜 b

theorem SetLike.Homogeneous.prod {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] {s : Finset A} (hs : ∀ x ∈ s, SetLike.Homogeneous 𝒜 x) : SetLike.Homogeneous 𝒜 (∏ i ∈ s, i)

theorem SetLike.Homogeneous.prod' {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] {n : ℕ} (v : Fin n → A) (hs : ∀ (i : Fin n), SetLike.Homogeneous 𝒜 (v i)) : SetLike.Homogeneous 𝒜 (∏ i : Fin n, v i)

theorem SetLike.Homogeneous.pow {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] {a : A} (ha : SetLike.Homogeneous 𝒜 a) (n : ℕ) : SetLike.Homogeneous 𝒜 (a ^ n)

theorem SetLike.Homogeneous.prod'' {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] {ι✝ : Type u_4} (f : ι✝ → A) {s : Finset ι✝} (hs : ∀ x ∈ s, SetLike.Homogeneous 𝒜 (f x)) : SetLike.Homogeneous 𝒜 (∏ i ∈ s, f i)