R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ ¬f ∈ ↑I.asHomogeneousIdeal ↔ ¬f ∈ I.asHomogeneousIdeal
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ I ∈ zeroLocus 𝒜 {f}ᶜ ↔ ¬f ∈ I.asHomogeneousIdeal
rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]
no goals
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ ¬f ∈ ↑I.asHomogeneousIdeal ↔ ¬f ∈ I.asHomogeneousIdeal
rfl