@[simp]

theorem HomogeneousLocalization.NumDenSameDeg.deg_prod {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (x : Submonoid A) {ι✝ : Type u_4} (s : Finset ι✝) (f : ι✝ → HomogeneousLocalization.NumDenSameDeg 𝒜 x) : (∏ i ∈ s, f i).deg = ∑ i ∈ s, (f i).deg

@[simp]

theorem HomogeneousLocalization.NumDenSameDeg.num_prod {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (x : Submonoid A) {ι✝ : Type u_4} (s : Finset ι✝) (f : ι✝ → HomogeneousLocalization.NumDenSameDeg 𝒜 x) : (∏ i ∈ s, f i).num = ⟨∏ i ∈ s, ↑(f i).num, ⋯⟩

@[simp]

theorem HomogeneousLocalization.NumDenSameDeg.den_prod {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (x : Submonoid A) {ι✝ : Type u_4} (s : Finset ι✝) (f : ι✝ → HomogeneousLocalization.NumDenSameDeg 𝒜 x) : (∏ i ∈ s, f i).den = ⟨∏ i ∈ s, ↑(f i).den, ⋯⟩

theorem HomogeneousLocalization.prod_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (x : Submonoid A) {ι✝ : Type u_4} (s : Finset ι✝) (f : ι✝ → HomogeneousLocalization.NumDenSameDeg 𝒜 x) : ∏ i ∈ s, HomogeneousLocalization.mk (f i) = HomogeneousLocalization.mk (∏ i ∈ s, f i)