ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_3<VAR>Semiring k<VAR>AddMonoid G<VAR>Semiring R<VAR>f g : AddMonoidAlgebra k G →+* R<VAR>h₁ : f.comp AddMonoidAlgebra.singleZeroRingHom = g.comp AddMonoidAlgebra.singleZeroRingHom<VAR>h_of : (↑f).comp (AddMonoidAlgebra.of k G) = (↑g).comp (AddMonoidAlgebra.of k G)<GOAL>f = g
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddCommMonoid G<GOAL>∀ (a : G →₀ kᵐᵒᵖ), AddMonoidAlgebra.opRingEquiv.symm a = MulOpposite.op (Finsupp.mapRange MulOpposite.unop ⋯ a)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddCommMonoid G<GOAL>∀ (a : (G →₀ k)ᵐᵒᵖ), AddMonoidAlgebra.opRingEquiv a = Finsupp.mapRange MulOpposite.op ⋯ (MulOpposite.unop a)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddCommMonoid G<VAR>r : k<VAR>x : G<GOAL>AddMonoidAlgebra.opRingEquiv (MulOpposite.op (AddMonoidAlgebra.single x r)) = AddMonoidAlgebra.single x (MulOpposite.op r)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>Semiring k<VAR>AddCommMonoid G<VAR>r : kᵐᵒᵖ<VAR>x : Gᵐᵒᵖ<GOAL>AddMonoidAlgebra.opRingEquiv.symm (AddMonoidAlgebra.single x r) = MulOpposite.op (AddMonoidAlgebra.single x (MulOpposite.unop r))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Semiring k<VAR>Algebra R k<VAR>AddMonoid G<GOAL>∀ (a : k), AddMonoidAlgebra.singleZeroAlgHom a = Finsupp.single 0 a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Semiring k<VAR>Algebra R k<VAR>AddMonoid G<GOAL>⇑(algebraMap R (AddMonoidAlgebra k G)) = AddMonoidAlgebra.single 0 ∘ ⇑(algebraMap R k)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>φ₁ φ₂ : AddMonoidAlgebra k G →ₐ[k] A<VAR>h : ∀ (x : G), φ₁ (AddMonoidAlgebra.single x 1) = φ₂ (AddMonoidAlgebra.single x 1)<GOAL>φ₁ = φ₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>φ₁ φ₂ : AddMonoidAlgebra k G →ₐ[k] A<VAR>h : (↑φ₁).comp (AddMonoidAlgebra.of k G) = (↑φ₂).comp (AddMonoidAlgebra.of k G)<GOAL>φ₁ = φ₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : Multiplicative G →* A<VAR>f : MonoidAlgebra k G<GOAL>((AddMonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => (algebraMap k A) b * F (Multiplicative.ofAdd a)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : Multiplicative G →* A<VAR>f : MonoidAlgebra k G<GOAL>((AddMonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => b • F (Multiplicative.ofAdd a)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : Multiplicative G →* A<GOAL>⇑((AddMonoidAlgebra.lift k G A) F) = ⇑(AddMonoidAlgebra.liftNC ↑(algebraMap k A) ⇑F)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : AddMonoidAlgebra k G →ₐ[k] A<VAR>x : Multiplicative G<GOAL>((AddMonoidAlgebra.lift k G A).symm F) x = F (AddMonoidAlgebra.single (Multiplicative.toAdd x) 1)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : Multiplicative G →* A<VAR>x : Multiplicative G<GOAL>((AddMonoidAlgebra.lift k G A) F) ((AddMonoidAlgebra.of k G) x) = F x
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : Multiplicative G →* A<VAR>a : G<VAR>b : k<GOAL>((AddMonoidAlgebra.lift k G A) F) (AddMonoidAlgebra.single a b) = b • F (Multiplicative.ofAdd a)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : Multiplicative G →* A<VAR>x : G<GOAL>((AddMonoidAlgebra.lift k G A) F) (AddMonoidAlgebra.of' k G x) = F (Multiplicative.ofAdd x)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : AddMonoidAlgebra k G →ₐ[k] A<GOAL>F = (AddMonoidAlgebra.lift k G A) ((↑F).comp (AddMonoidAlgebra.of k G))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>F : AddMonoidAlgebra k G →ₐ[k] A<VAR>f : MonoidAlgebra k G<GOAL>F f = Finsupp.sum f fun a b => b • F (AddMonoidAlgebra.single a 1)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>CommSemiring k<VAR>AddMonoid G<VAR>A : Type u₃<VAR>Semiring A<VAR>Algebra k A<VAR>φ₁ φ₂ : AddMonoidAlgebra k G →ₐ[k] A<GOAL>(∀ (x : G), φ₁ (Finsupp.single x 1) = φ₂ (Finsupp.single x 1)) ↔ φ₁ = φ₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>ι : Type ui<VAR>CommSemiring k<VAR>AddCommMonoid G<VAR>s : Finset ι<VAR>a : ι → G<VAR>b : ι → k<GOAL>∏ i ∈ s, AddMonoidAlgebra.single (a i) (b i) = AddMonoidAlgebra.single (∑ i ∈ s, a i) (∏ i ∈ s, b i)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>A : Type u_3<VAR>H : Type u_4<VAR>F : Type u_5<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<VAR>AddMonoid G<VAR>AddMonoid H<VAR>FunLike F G H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>r : k<GOAL>AddMonoidAlgebra.mapDomain (⇑f) ((algebraMap k (AddMonoidAlgebra A G)) r) = (algebraMap k (AddMonoidAlgebra A H)) r
<VAR>k : Type u_3<VAR>A : Type u_4<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<VAR>G : Type u_5<VAR>H : Type u_6<VAR>F : Type u_7<VAR>Add G<VAR>Add H<VAR>FunLike F G H<VAR>AddHomClass F G H<VAR>f : F<GOAL>∀ (a : G →₀ A), (AddMonoidAlgebra.mapDomainNonUnitalAlgHom k A f) a = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a
<VAR>G : Type u₂<VAR>k : Type u_3<VAR>A : Type u_4<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<VAR>AddMonoid G<VAR>H : Type u_5<VAR>F : Type u_6<VAR>AddMonoid H<VAR>FunLike F G H<VAR>AddMonoidHomClass F G H<VAR>f : F<GOAL>∀ (a : G →₀ A), (AddMonoidAlgebra.mapDomainAlgHom k A f) a = Finsupp.mapDomain (⇑f) a
<VAR>G : Type u₂<VAR>k : Type u_3<VAR>A : Type u_4<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<VAR>AddMonoid G<GOAL>AddMonoidAlgebra.mapDomainAlgHom k A (AddMonoidHom.id G) = AlgHom.id k (AddMonoidAlgebra A G)
<VAR>k : Type u_3<VAR>A : Type u_4<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>CommSemiring k<VAR>Semiring A<VAR>Algebra k A<VAR>AddMonoid G₁<VAR>AddMonoid G₂<VAR>AddMonoid G₃<VAR>f : G₁ →+ G₂<VAR>g : G₂ →+ G₃<GOAL>AddMonoidAlgebra.mapDomainAlgHom k A (g.comp f) = (AddMonoidAlgebra.mapDomainAlgHom k A g).comp (AddMonoidAlgebra.mapDomainAlgHom k A f)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>A : Type u_3<VAR>CommSemiring k<VAR>AddMonoid G<VAR>AddMonoid H<VAR>Semiring A<VAR>Algebra k A<VAR>e : G ≃+ H<GOAL>↑(AddMonoidAlgebra.domCongr k A e) = AddMonoidAlgebra.mapDomainAlgHom k A e
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>A : Type u_3<VAR>CommSemiring k<VAR>AddMonoid G<VAR>AddMonoid H<VAR>Semiring A<VAR>Algebra k A<VAR>e : G ≃+ H<VAR>f : MonoidAlgebra A G<VAR>h : H<GOAL>((AddMonoidAlgebra.domCongr k A e) f) h = f (e.symm h)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>A : Type u_3<VAR>CommSemiring k<VAR>AddMonoid G<VAR>AddMonoid H<VAR>Semiring A<VAR>Algebra k A<VAR>e : G ≃+ H<VAR>f : MonoidAlgebra A G<GOAL>((AddMonoidAlgebra.domCongr k A e) f).support = Finset.map (↑e).toEmbedding f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>A : Type u_3<VAR>CommSemiring k<VAR>AddMonoid G<VAR>AddMonoid H<VAR>Semiring A<VAR>Algebra k A<VAR>e : G ≃+ H<VAR>g : G<VAR>a : A<GOAL>(AddMonoidAlgebra.domCongr k A e) (AddMonoidAlgebra.single g a) = AddMonoidAlgebra.single (e g) a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>A : Type u_3<VAR>CommSemiring k<VAR>AddMonoid G<VAR>Semiring A<VAR>Algebra k A<GOAL>AddMonoidAlgebra.domCongr k A (AddEquiv.refl G) = AlgEquiv.refl
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>A : Type u_3<VAR>CommSemiring k<VAR>AddMonoid G<VAR>AddMonoid H<VAR>Semiring A<VAR>Algebra k A<VAR>e : G ≃+ H<GOAL>(AddMonoidAlgebra.domCongr k A e).symm = AddMonoidAlgebra.domCongr k A e.symm
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>CommRing T<VAR>Algebra R T<GOAL>Continuous (PrimeSpectrum.tensorProductTo R S T)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>CommRing T<VAR>Algebra R T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>p₁ p₂ : PrimeSpectrum (S ⊗[R] T)<VAR>h : PrimeSpectrum.tensorProductTo R S T p₁ = PrimeSpectrum.tensorProductTo R S T p₂<GOAL>p₁ ≤ p₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>CommRing T<VAR>Algebra R T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<GOAL>Embedding (PrimeSpectrum.tensorProductTo R S T)
<VAR>R : Type u<VAR>CommSemiring R<VAR>U : Set (PrimeSpectrum R)<GOAL>IsOpen U ↔ ∃ s, Uᶜ = PrimeSpectrum.zeroLocus s
<VAR>R : Type u<VAR>CommSemiring R<VAR>Z : Set (PrimeSpectrum R)<GOAL>IsClosed Z ↔ ∃ s, Z = PrimeSpectrum.zeroLocus s
<VAR>R : Type u<VAR>CommSemiring R<VAR>Z : Set (PrimeSpectrum R)<GOAL>IsClosed Z ↔ ∃ I, Z = PrimeSpectrum.zeroLocus ↑I
<VAR>R : Type u<VAR>CommSemiring R<VAR>Z : Set (PrimeSpectrum R)<GOAL>IsClosed Z ↔ ∃ I, I.IsRadical ∧ Z = PrimeSpectrum.zeroLocus ↑I
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set R<GOAL>IsClosed (PrimeSpectrum.zeroLocus s)
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Set (PrimeSpectrum R)<GOAL>PrimeSpectrum.zeroLocus ↑(PrimeSpectrum.vanishingIdeal t) = closure t
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Set (PrimeSpectrum R)<GOAL>PrimeSpectrum.vanishingIdeal (closure t) = PrimeSpectrum.vanishingIdeal t
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : PrimeSpectrum R<GOAL>closure {x} = PrimeSpectrum.zeroLocus ↑x.asIdeal
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : PrimeSpectrum R<GOAL>IsClosed {x} ↔ x.asIdeal.IsMaximal
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set (PrimeSpectrum R)<GOAL>(PrimeSpectrum.vanishingIdeal s).IsRadical
<VAR>R : Type u<VAR>CommSemiring R<VAR>s t : Set (PrimeSpectrum R)<VAR>ht : IsClosed t<GOAL>s ⊆ t ↔ PrimeSpectrum.vanishingIdeal t ≤ PrimeSpectrum.vanishingIdeal s
<VAR>R : Type u<VAR>CommSemiring R<VAR>s t : Set (PrimeSpectrum R)<VAR>hs : IsClosed s<VAR>ht : IsClosed t<GOAL>s ⊂ t ↔ PrimeSpectrum.vanishingIdeal t < PrimeSpectrum.vanishingIdeal s
<VAR>R : Type u<VAR>CommSemiring R<VAR>IsDomain R<GOAL>T1Space (PrimeSpectrum R) ↔ IsField R
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsRadical<GOAL>IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ I.IsPrime
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ I.radical.IsPrime
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set (PrimeSpectrum R)<GOAL>IsIrreducible s ↔ (PrimeSpectrum.vanishingIdeal s).IsPrime
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.vanishingIdeal '' {s | IsIrreducible s} = {P | P.IsPrime}
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s} = {P | P.IsPrime}
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>s : Set R<GOAL>(fun y => { asIdeal := Ideal.comap f y.asIdeal, isPrime := ⋯ }) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus (⇑f '' s)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>y : PrimeSpectrum S<GOAL>((PrimeSpectrum.comap f) y).asIdeal = Ideal.comap f y.asIdeal
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.comap (RingHom.id R) = ContinuousMap.id (PrimeSpectrum R)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>S' : Type u_1<VAR>CommSemiring S'<VAR>f : R →+* S<VAR>g : S →+* S'<GOAL>PrimeSpectrum.comap (g.comp f) = (PrimeSpectrum.comap f).comp (PrimeSpectrum.comap g)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>S' : Type u_1<VAR>CommSemiring S'<VAR>f : R →+* S<VAR>g : S →+* S'<VAR>x : PrimeSpectrum S'<GOAL>(PrimeSpectrum.comap (g.comp f)) x = (PrimeSpectrum.comap f) ((PrimeSpectrum.comap g) x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>s : Set R<GOAL>⇑(PrimeSpectrum.comap f) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus (⇑f '' s)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective ⇑(PrimeSpectrum.comap f)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>M : Submonoid R<VAR>IsLocalization M S<GOAL>Inducing ⇑(PrimeSpectrum.comap (algebraMap R S))
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>M : Submonoid R<VAR>IsLocalization M S<GOAL>Function.Injective ⇑(PrimeSpectrum.comap (algebraMap R S))
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>M : Submonoid R<VAR>IsLocalization M S<GOAL>Embedding ⇑(PrimeSpectrum.comap (algebraMap R S))
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>M : Submonoid R<VAR>IsLocalization M S<GOAL>Set.range ⇑(PrimeSpectrum.comap (algebraMap R S)) = {p | Disjoint ↑M ↑p.asIdeal}
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>Inducing ⇑(PrimeSpectrum.comap f)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>x : PrimeSpectrum S<VAR>hx : IsClosed {x}<GOAL>IsClosed {(PrimeSpectrum.comap f) x}
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : f.IsIntegral<VAR>x : PrimeSpectrum S<VAR>hx : IsClosed {x}<GOAL>IsClosed {(PrimeSpectrum.comap f) x}
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal S<GOAL>⇑(PrimeSpectrum.comap f) '' PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑(Ideal.comap f I)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>Set.range ⇑(PrimeSpectrum.comap f) = PrimeSpectrum.zeroLocus ↑(RingHom.ker f)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>IsClosed (Set.range ⇑(PrimeSpectrum.comap f))
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>ClosedEmbedding ⇑(PrimeSpectrum.comap f)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>x : PrimeSpectrum R<GOAL>(PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x) = (PrimeSpectrum.comap (RingHom.fst R S)) x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>x : PrimeSpectrum S<GOAL>(PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x) = (PrimeSpectrum.comap (RingHom.snd R S)) x
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R<VAR>x : PrimeSpectrum R<GOAL>x ∈ PrimeSpectrum.basicOpen f ↔ f ∉ x.asIdeal
<VAR>R : Type u<VAR>CommSemiring R<VAR>a : R<GOAL>IsOpen ↑(PrimeSpectrum.basicOpen a)
<VAR>R : Type u<VAR>CommSemiring R<VAR>r : R<GOAL>↑(PrimeSpectrum.basicOpen r) = (PrimeSpectrum.zeroLocus {r})ᶜ
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.basicOpen 1 = ⊤
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.basicOpen 0 = ⊥
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R<GOAL>PrimeSpectrum.basicOpen f ≤ PrimeSpectrum.basicOpen g ↔ f ∈ (Ideal.span {g}).radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R<GOAL>PrimeSpectrum.basicOpen (f * g) = PrimeSpectrum.basicOpen f ⊓ PrimeSpectrum.basicOpen g
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R<GOAL>PrimeSpectrum.basicOpen (f * g) ≤ PrimeSpectrum.basicOpen f
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R<GOAL>PrimeSpectrum.basicOpen (f * g) ≤ PrimeSpectrum.basicOpen g
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>PrimeSpectrum.basicOpen (f ^ n) = PrimeSpectrum.basicOpen f
<VAR>R : Type u<VAR>CommSemiring R<GOAL>TopologicalSpace.IsTopologicalBasis (Set.range fun r => ↑(PrimeSpectrum.basicOpen r))
<VAR>R : Type u<VAR>CommSemiring R<GOAL>TopologicalSpace.Opens.IsBasis (Set.range PrimeSpectrum.basicOpen)
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R<GOAL>PrimeSpectrum.basicOpen f = ⊥ ↔ IsNilpotent f
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type v<VAR>CommSemiring S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<GOAL>Set.range ⇑(PrimeSpectrum.comap (algebraMap R S)) = ↑(PrimeSpectrum.basicOpen r)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type v<VAR>CommSemiring S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<GOAL>OpenEmbedding ⇑(PrimeSpectrum.comap (algebraMap R S))
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R<GOAL>IsCompact ↑(PrimeSpectrum.basicOpen f)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>x : R<GOAL>(TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) (PrimeSpectrum.basicOpen x) = PrimeSpectrum.basicOpen (f x)
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Type u_1<VAR>f : ι → R<GOAL>⨆ i, PrimeSpectrum.basicOpen (f i) = ⊤ ↔ Ideal.span (Set.range f) = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set R<GOAL>⨆ i ∈ s, PrimeSpectrum.basicOpen i = ⊤ ↔ Ideal.span s = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : PrimeSpectrum R<GOAL>x ≤ y ↔ y ∈ closure {x}
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : PrimeSpectrum R<GOAL>x ≤ y ↔ x ⤳ y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : PrimeSpectrum R<GOAL>PrimeSpectrum.nhdsOrderEmbedding x = nhds x
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.vanishingIdeal '' irreducibleComponents (PrimeSpectrum R) = minimalPrimes R
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.zeroLocus ∘ SetLike.coe '' minimalPrimes R = irreducibleComponents (PrimeSpectrum R)
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set (PrimeSpectrum R)<GOAL>PrimeSpectrum.vanishingIdeal s ∈ minimalPrimes R ↔ closure s ∈ irreducibleComponents (PrimeSpectrum R)
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>PrimeSpectrum.zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ I.radical ∈ minimalPrimes R
<VAR>R : Type u<VAR>CommSemiring R<VAR>LocalRing R<VAR>S : Type v<VAR>CommSemiring S<VAR>LocalRing S<VAR>f : R →+* S<GOAL>IsLocalRingHom f ↔ (PrimeSpectrum.comap f) (LocalRing.closedPoint S) = LocalRing.closedPoint R
<VAR>R : Type u<VAR>CommSemiring R<VAR>LocalRing R<VAR>S : Type v<VAR>CommSemiring S<VAR>LocalRing S<VAR>f : R →+* S<VAR>IsLocalRingHom f<GOAL>(PrimeSpectrum.comap f) (LocalRing.closedPoint S) = LocalRing.closedPoint R
<VAR>R : Type u<VAR>CommSemiring R<VAR>LocalRing R<VAR>x : PrimeSpectrum R<GOAL>x ⤳ LocalRing.closedPoint R
<VAR>R : Type u<VAR>CommSemiring R<VAR>LocalRing R<VAR>U : TopologicalSpace.Opens (PrimeSpectrum R)<GOAL>LocalRing.closedPoint R ∈ U ↔ U = ⊤
<VAR>T : Type u<VAR>CommRing T<VAR>LocalRing T<VAR>x : PrimeSpectrum (LocalRing.ResidueField T)<GOAL>(PrimeSpectrum.comap (LocalRing.residue T)) x = LocalRing.closedPoint T
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Multiset α<VAR>hs : s.Nodup<VAR>f : α → β<GOAL>{ val := s, nodup := hs }.sum f = (Multiset.map f s).sum
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Multiset α<VAR>hs : s.Nodup<VAR>f : α → β<GOAL>{ val := s, nodup := hs }.prod f = (Multiset.map f s).prod
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Finset α<GOAL>s.val.prod = s.prod id
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Finset α<GOAL>s.val.sum = s.sum id
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>∑ x ∈ s, f x = (Multiset.map f s.val).sum
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>∏ x ∈ s, f x = (Multiset.map f s.val).prod
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>(Multiset.map f s.val).prod = ∏ a ∈ s, f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>(Multiset.map f s.val).sum = ∑ a ∈ s, f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>∑ x ∈ s, f x = Finset.fold (fun x x_1 => x + x_1) 0 f s
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>∏ x ∈ s, f x = Finset.fold (fun x x_1 => x * x_1) 1 f s
<VAR>α : Type u_3<VAR>s : Finset α<GOAL>∑ x ∈ s, {x} = s.val
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid β<VAR>CommMonoid γ<VAR>G : Type u_6<VAR>FunLike G β γ<VAR>MonoidHomClass G β γ<VAR>g : G<VAR>f : α → β<VAR>s : Finset α<GOAL>g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid β<VAR>AddCommMonoid γ<VAR>G : Type u_6<VAR>FunLike G β γ<VAR>AddMonoidHomClass G β γ<VAR>g : G<VAR>f : α → β<VAR>s : Finset α<GOAL>g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddZeroClass β<VAR>AddCommMonoid γ<VAR>f : α → β →+ γ<VAR>s : Finset α<GOAL>⇑(∑ x ∈ s, f x) = ∑ x ∈ s, ⇑(f x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>MulOneClass β<VAR>CommMonoid γ<VAR>f : α → β →* γ<VAR>s : Finset α<GOAL>⇑(∏ x ∈ s, f x) = ∏ x ∈ s, ⇑(f x)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddZeroClass β<VAR>AddCommMonoid γ<VAR>f : α → β →+ γ<VAR>s : Finset α<VAR>b : β<GOAL>(∑ x ∈ s, f x) b = ∑ x ∈ s, (f x) b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>MulOneClass β<VAR>CommMonoid γ<VAR>f : α → β →* γ<VAR>s : Finset α<VAR>b : β<GOAL>(∏ x ∈ s, f x) b = ∏ x ∈ s, (f x) b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>AddCommMonoid β<GOAL>∑ x ∈ ∅, f x = 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>CommMonoid β<GOAL>∏ x ∈ ∅, f x = 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>CommMonoid β<VAR>IsEmpty α<VAR>s : Finset α<GOAL>∏ i ∈ s, f i = 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>AddCommMonoid β<VAR>IsEmpty α<VAR>s : Finset α<GOAL>∑ i ∈ s, f i = 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>CommMonoid β<VAR>h : a ∉ s<GOAL>∏ x ∈ Finset.cons a s h, f x = f a * ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>h : a ∉ s<GOAL>∑ x ∈ Finset.cons a s h, f x = f a + ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>CommMonoid β<VAR>DecidableEq α<GOAL>a ∉ s → ∏ x ∈ insert a s, f x = f a * ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>DecidableEq α<GOAL>a ∉ s → ∑ x ∈ insert a s, f x = f a + ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>h : a ∉ s → f a = 0<GOAL>∑ x ∈ insert a s, f x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>CommMonoid β<VAR>DecidableEq α<VAR>h : a ∉ s → f a = 1<GOAL>∏ x ∈ insert a s, f x = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>CommMonoid β<VAR>DecidableEq α<VAR>h : f a = 1<GOAL>∏ x ∈ insert a s, f x = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>h : f a = 0<GOAL>∑ x ∈ insert a s, f x = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>s : Finset α<VAR>a : α<VAR>M : Type u_6<VAR>CommGroup M<VAR>DecidableEq α<VAR>ha : a ∉ s<VAR>f : α → M<GOAL>(∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x
<VAR>α : Type u_3<VAR>s : Finset α<VAR>a : α<VAR>M : Type u_6<VAR>AddCommGroup M<VAR>DecidableEq α<VAR>ha : a ∉ s<VAR>f : α → M<GOAL>∑ x ∈ insert a s, f x - f a = ∑ x ∈ s, f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid β<VAR>f : α → β<VAR>a : α<GOAL>∑ x ∈ {a}, f x = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>f : α → β<VAR>a : α<GOAL>∏ x ∈ {a}, f x = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>AddCommMonoid β<VAR>DecidableEq α<VAR>a b : α<VAR>h : a ≠ b<GOAL>∑ x ∈ {a, b}, f x = f a + f b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>CommMonoid β<VAR>DecidableEq α<VAR>a b : α<VAR>h : a ≠ b<GOAL>∏ x ∈ {a, b}, f x = f a * f b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>CommMonoid β<GOAL>∏ _x ∈ s, 1 = 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : Finset α<VAR>AddCommMonoid β<GOAL>∑ _x ∈ s, 0 = 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>CommMonoid β<VAR>DecidableEq α<VAR>s : Finset γ<VAR>g : γ → α<GOAL>(∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ∏ x ∈ Finset.image g s, f x = ∏ x ∈ s, f (g x)