ι : Type u_2
σ : Type u_3
R : Type ?u.130786
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ (I : Ideal A), I ∈ ℐ → IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨅ (a : Ideal A) (_ : a ∈ ℐ), a)
ι : Type u_2
σ : Type u_3
R : Type ?u.130786
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ (I : Ideal A), I ∈ ℐ → IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (InfSet.sInf ℐ)
rw [sInf_eq_iInf]
no goals
ι : Type u_2
σ : Type u_3
R : Type ?u.130786
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ (I : Ideal A), I ∈ ℐ → IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨅ (a : Ideal A) (_ : a ∈ ℐ), a)
exact iInf₂ h