ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>self : ProjectiveSpectrum 𝒜<GOAL>self.asHomogeneousIdeal.toIdeal.IsPrime
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>self : ProjectiveSpectrum 𝒜<GOAL>¬HomogeneousIdeal.irrelevant 𝒜 ≤ self.asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : ProjectiveSpectrum 𝒜<VAR>s : Set A<GOAL>x ∈ ProjectiveSpectrum.zeroLocus 𝒜 s ↔ s ⊆ ↑x.asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>s : Set A<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑(Ideal.span s) = ProjectiveSpectrum.zeroLocus 𝒜 s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<GOAL>↑(ProjectiveSpectrum.vanishingIdeal t) = {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<VAR>f : A<GOAL>f ∈ ProjectiveSpectrum.vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : ProjectiveSpectrum 𝒜<GOAL>ProjectiveSpectrum.vanishingIdeal {x} = x.asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<VAR>I : Ideal A<GOAL>t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 ↑I ↔ I ≤ (ProjectiveSpectrum.vanishingIdeal t).toIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>GaloisConnection (fun I => ProjectiveSpectrum.zeroLocus 𝒜 ↑I) fun t => (ProjectiveSpectrum.vanishingIdeal t).toIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>GaloisConnection (fun s => ProjectiveSpectrum.zeroLocus 𝒜 s) fun t => ↑(ProjectiveSpectrum.vanishingIdeal t)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>GaloisConnection (fun I => ProjectiveSpectrum.zeroLocus 𝒜 ↑I) fun t => ProjectiveSpectrum.vanishingIdeal t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<VAR>s : Set A<GOAL>t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 s ↔ s ⊆ ↑(ProjectiveSpectrum.vanishingIdeal t)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>s : Set A<GOAL>s ⊆ ↑(ProjectiveSpectrum.vanishingIdeal (ProjectiveSpectrum.zeroLocus 𝒜 s))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>I : Ideal A<GOAL>I ≤ (ProjectiveSpectrum.vanishingIdeal (ProjectiveSpectrum.zeroLocus 𝒜 ↑I)).toIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>I : HomogeneousIdeal 𝒜<GOAL>I ≤ ProjectiveSpectrum.vanishingIdeal (ProjectiveSpectrum.zeroLocus 𝒜 ↑I)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<GOAL>t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 ↑(ProjectiveSpectrum.vanishingIdeal t)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>s t : Set A<VAR>h : s ⊆ t<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>s t : Ideal A<VAR>h : s ≤ t<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 ↑s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>s t : HomogeneousIdeal 𝒜<VAR>h : s ≤ t<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 ↑s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>s t : Set (ProjectiveSpectrum 𝒜)<VAR>h : s ⊆ t<GOAL>ProjectiveSpectrum.vanishingIdeal t ≤ ProjectiveSpectrum.vanishingIdeal s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑⊥ = Set.univ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 {0} = Set.univ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ∅ = Set.univ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>ProjectiveSpectrum.vanishingIdeal ∅ = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>s : Set A<VAR>h : 1 ∈ s<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 s = ∅
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 {1} = ∅
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 Set.univ = ∅
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>I J : Ideal A<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑(I ⊔ J) = ProjectiveSpectrum.zeroLocus 𝒜 ↑I ∩ ProjectiveSpectrum.zeroLocus 𝒜 ↑J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>I J : HomogeneousIdeal 𝒜<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑(I ⊔ J) = ProjectiveSpectrum.zeroLocus 𝒜 ↑I ∩ ProjectiveSpectrum.zeroLocus 𝒜 ↑J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>s s' : Set A<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 (s ∪ s') = ProjectiveSpectrum.zeroLocus 𝒜 s ∩ ProjectiveSpectrum.zeroLocus 𝒜 s'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>t t' : Set (ProjectiveSpectrum 𝒜)<GOAL>ProjectiveSpectrum.vanishingIdeal (t ∪ t') = ProjectiveSpectrum.vanishingIdeal t ⊓ ProjectiveSpectrum.vanishingIdeal t'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>γ : Sort u_3<VAR>I : γ → Ideal A<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑(⨆ i, I i) = ⋂ i, ProjectiveSpectrum.zeroLocus 𝒜 ↑(I i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>γ : Sort u_3<VAR>I : γ → HomogeneousIdeal 𝒜<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑(⨆ i, I i) = ⋂ i, ProjectiveSpectrum.zeroLocus 𝒜 ↑(I i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>γ : Sort u_3<VAR>s : γ → Set A<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 (⋃ i, s i) = ⋂ i, ProjectiveSpectrum.zeroLocus 𝒜 (s i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>s : Set (Set A)<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 (⋃ s' ∈ s, s') = ⋂ s' ∈ s, ProjectiveSpectrum.zeroLocus 𝒜 s'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>γ : Sort u_3<VAR>t : γ → Set (ProjectiveSpectrum 𝒜)<GOAL>ProjectiveSpectrum.vanishingIdeal (⋃ i, t i) = ⨅ i, ProjectiveSpectrum.vanishingIdeal (t i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>I J : Ideal A<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑(I ⊓ J) = ProjectiveSpectrum.zeroLocus 𝒜 ↑I ∪ ProjectiveSpectrum.zeroLocus 𝒜 ↑J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>s s' : Set A<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 s ∪ ProjectiveSpectrum.zeroLocus 𝒜 s' = ProjectiveSpectrum.zeroLocus 𝒜 ↑(Ideal.span s ⊓ Ideal.span s')
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>I J : Ideal A<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑(I * J) = ProjectiveSpectrum.zeroLocus 𝒜 ↑I ∪ ProjectiveSpectrum.zeroLocus 𝒜 ↑J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>I J : HomogeneousIdeal 𝒜<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑(I * J) = ProjectiveSpectrum.zeroLocus 𝒜 ↑I ∪ ProjectiveSpectrum.zeroLocus 𝒜 ↑J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f g : A<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 {f * g} = ProjectiveSpectrum.zeroLocus 𝒜 {f} ∪ ProjectiveSpectrum.zeroLocus 𝒜 {g}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 {f ^ n} = ProjectiveSpectrum.zeroLocus 𝒜 {f}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>t t' : Set (ProjectiveSpectrum 𝒜)<GOAL>ProjectiveSpectrum.vanishingIdeal t ⊔ ProjectiveSpectrum.vanishingIdeal t' ≤ ProjectiveSpectrum.vanishingIdeal (t ∩ t')
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>I : ProjectiveSpectrum 𝒜<GOAL>I ∈ (ProjectiveSpectrum.zeroLocus 𝒜 {f})ᶜ ↔ f ∉ I.asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>U : Set (ProjectiveSpectrum 𝒜)<GOAL>IsOpen U ↔ ∃ s, Uᶜ = ProjectiveSpectrum.zeroLocus 𝒜 s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>Z : Set (ProjectiveSpectrum 𝒜)<GOAL>IsClosed Z ↔ ∃ s, Z = ProjectiveSpectrum.zeroLocus 𝒜 s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>s : Set A<GOAL>IsClosed (ProjectiveSpectrum.zeroLocus 𝒜 s)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<GOAL>ProjectiveSpectrum.zeroLocus 𝒜 ↑(ProjectiveSpectrum.vanishingIdeal t) = closure t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<GOAL>ProjectiveSpectrum.vanishingIdeal (closure t) = ProjectiveSpectrum.vanishingIdeal t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ProjectiveSpectrum 𝒜<GOAL>x ∈ ProjectiveSpectrum.basicOpen 𝒜 f ↔ f ∉ x.asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ProjectiveSpectrum 𝒜<GOAL>x ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 f) ↔ f ∉ x.asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>a : A<GOAL>IsOpen ↑(ProjectiveSpectrum.basicOpen 𝒜 a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>r : A<GOAL>↑(ProjectiveSpectrum.basicOpen 𝒜 r) = (ProjectiveSpectrum.zeroLocus 𝒜 {r})ᶜ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>ProjectiveSpectrum.basicOpen 𝒜 1 = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>ProjectiveSpectrum.basicOpen 𝒜 0 = ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f g : A<GOAL>ProjectiveSpectrum.basicOpen 𝒜 (f * g) = ProjectiveSpectrum.basicOpen 𝒜 f ⊓ ProjectiveSpectrum.basicOpen 𝒜 g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f g : A<GOAL>ProjectiveSpectrum.basicOpen 𝒜 (f * g) ≤ ProjectiveSpectrum.basicOpen 𝒜 f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f g : A<GOAL>ProjectiveSpectrum.basicOpen 𝒜 (f * g) ≤ ProjectiveSpectrum.basicOpen 𝒜 g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>ProjectiveSpectrum.basicOpen 𝒜 (f ^ n) = ProjectiveSpectrum.basicOpen 𝒜 f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<GOAL>ProjectiveSpectrum.basicOpen 𝒜 f = ⨆ i, ProjectiveSpectrum.basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<GOAL>TopologicalSpace.IsTopologicalBasis (Set.range fun r => ↑(ProjectiveSpectrum.basicOpen 𝒜 r))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x y : ProjectiveSpectrum 𝒜<GOAL>x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ x ≤ y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x y : ProjectiveSpectrum 𝒜<GOAL>x.asHomogeneousIdeal < y.asHomogeneousIdeal ↔ x < y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x y : ProjectiveSpectrum 𝒜<GOAL>x ≤ y ↔ y ∈ closure {x}
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>a b : α<GOAL>s(a, b).sup = a ⊔ b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>a b : α<GOAL>s(a, b).inf = a ⊓ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>s : Sym2 α<GOAL>s.inf ≤ s.sup
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>p : { p // p.1 ≤ p.2 }<GOAL>Sym2.sortEquiv.symm p = Sym2.mk ↑p
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Sym2 α<GOAL>↑(Sym2.sortEquiv s) = (s.inf, s.sup)
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>a : R × R × R × R<GOAL>((QuaternionAlgebra.equivProd c₁ c₂).symm a).imJ = a.2.2.1
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>a : R × R × R × R<GOAL>((QuaternionAlgebra.equivProd c₁ c₂).symm a).imK = a.2.2.2
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>(QuaternionAlgebra.equivProd c₁ c₂) a = (a.re, a.imI, a.imJ, a.imK)
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>a : R × R × R × R<GOAL>((QuaternionAlgebra.equivProd c₁ c₂).symm a).re = a.1
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>a : R × R × R × R<GOAL>((QuaternionAlgebra.equivProd c₁ c₂).symm a).imI = a.2.1
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>a : Fin 4 → R<GOAL>(QuaternionAlgebra.equivTuple c₁ c₂).symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>x : ℍ[R,c₁,c₂]<GOAL>(QuaternionAlgebra.equivTuple c₁ c₂) x = ![x.re, x.imI, x.imJ, x.imK]
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>{ re := a.re, imI := a.imI, imJ := a.imJ, imK := a.imK } = a
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a.im.re = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a.im.imI = a.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a.im.imJ = a.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a.im.imK = a.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a.im.im = a.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x : R<GOAL>(↑x).re = x
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x : R<GOAL>(↑x).imI = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x : R<GOAL>(↑x).imJ = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x : R<GOAL>(↑x).imK = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>Function.Injective QuaternionAlgebra.coe
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ x y : R<GOAL>↑x = ↑y ↔ x = y
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>Quaternion.re 0 = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>Quaternion.imI 0 = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>Quaternion.imJ 0 = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>Quaternion.imK 0 = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>QuaternionAlgebra.im 0 = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>↑0 = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>Quaternion.re 1 = 1
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>Quaternion.imI 1 = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>Quaternion.imJ 1 = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>Quaternion.imK 1 = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>QuaternionAlgebra.im 1 = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>↑1 = 1
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a + b).re = a.re + b.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a + b).imI = a.imI + b.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a + b).imJ = a.imJ + b.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a + b).imK = a.imK + b.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a + b).im = a.im + b.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R<GOAL>{ re := a₁, imI := a₂, imJ := a₃, imK := a₄ } + { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } = { re := a₁ + b₁, imI := a₂ + b₂, imJ := a₃ + b₃, imK := a₄ + b₄ }
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x y : R<GOAL>↑(x + y) = ↑x + ↑y
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>(-a).re = -a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>(-a).imI = -a.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>(-a).imJ = -a.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>(-a).imK = -a.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>(-a).im = -a.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a₁ a₂ a₃ a₄ : R<GOAL>-{ re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = { re := -a₁, imI := -a₂, imJ := -a₃, imK := -a₄ }
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x : R<GOAL>↑(-x) = -↑x
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a - b).re = a.re - b.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a - b).imI = a.imI - b.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a - b).imJ = a.imJ - b.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a - b).imK = a.imK - b.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a - b).im = a.im - b.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R<GOAL>{ re := a₁, imI := a₂, imJ := a₃, imK := a₄ } - { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } = { re := a₁ - b₁, imI := a₂ - b₂, imJ := a₃ - b₃, imK := a₄ - b₄ }
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x : R<GOAL>(↑x).im = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>↑a.re + a.im = a
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a - a.im = ↑a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a - ↑a.re = a.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a * b).re = a.re * b.re + c₁ * a.imI * b.imI + c₂ * a.imJ * b.imJ - c₁ * c₂ * a.imK * b.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a * b).imI = a.re * b.imI + a.imI * b.re - c₂ * a.imJ * b.imK + c₂ * a.imK * b.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a * b).imJ = a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re - c₁ * a.imK * b.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a b : ℍ[R,c₁,c₂]<GOAL>(a * b).imK = a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R<GOAL>{ re := a₁, imI := a₂, imJ := a₃, imK := a₄ } * { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } = { re := a₁ * b₁ + c₁ * a₂ * b₂ + c₂ * a₃ * b₃ - c₁ * c₂ * a₄ * b₄, imI := a₁ * b₂ + a₂ * b₁ - c₂ * a₃ * b₄ + c₂ * a₄ * b₃, imJ := a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ - c₁ * a₄ * b₂, imK := a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁ }
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<VAR>SMul S R<VAR>s : S<GOAL>(s • a).re = s • a.re
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<VAR>SMul S R<VAR>s : S<GOAL>(s • a).imI = s • a.imI
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<VAR>SMul S R<VAR>s : S<GOAL>(s • a).imJ = s • a.imJ
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<VAR>SMul S R<VAR>s : S<GOAL>(s • a).imK = s • a.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<VAR>S : Type u_4<VAR>SMulZeroClass S R<VAR>s : S<GOAL>(s • a).im = s • a.im
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>c₁ c₂ : R<VAR>SMul S R<VAR>s : S<VAR>re im_i im_j im_k : R<GOAL>s • { re := re, imI := im_i, imJ := im_j, imK := im_k } = { re := s • re, imI := s • im_i, imJ := s • im_j, imK := s • im_k }
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>SMulZeroClass S R<VAR>s : S<VAR>r : R<GOAL>↑(s • r) = s • ↑r
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>n : ℕ<GOAL>(↑n).re = ↑n
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>n : ℕ<GOAL>(↑n).imI = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>n : ℕ<GOAL>(↑n).imJ = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>n : ℕ<GOAL>(↑n).imK = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>n : ℕ<GOAL>(↑n).im = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>z : ℤ<GOAL>(↑z).re = ↑z
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>z : ℤ<GOAL>(↑z).imI = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>z : ℤ<GOAL>(↑z).imJ = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>z : ℤ<GOAL>(↑z).imK = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>z : ℤ<GOAL>(↑z).im = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>z : ℤ<GOAL>↑↑z = ↑z
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x y : R<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>r : R<GOAL>(algebraMap R ℍ[R,c₁,c₂]) r = { re := r, imI := 0, imJ := 0, imK := 0 }
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>Function.Injective ⇑(algebraMap R ℍ[R,c₁,c₂])
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>self : ℍ[R,c₁,c₂]<GOAL>(QuaternionAlgebra.reₗ c₁ c₂) self = self.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>self : ℍ[R,c₁,c₂]<GOAL>(QuaternionAlgebra.imIₗ c₁ c₂) self = self.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>self : ℍ[R,c₁,c₂]<GOAL>(QuaternionAlgebra.imJₗ c₁ c₂) self = self.imJ