R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, zeroLocus 𝒜 s = Uᶜ
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, Uᶜ = zeroLocus 𝒜 s
simp only [@eq_comm _ (Uᶜ)]
no goals
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, zeroLocus 𝒜 s = Uᶜ
rfl