ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<VAR>Algebra S Sₘ<VAR>i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>Algebra Rₘ Sₘ<VAR>Algebra R Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<GOAL>IsLocalization.lift ⋯ = algebraMap Rₘ Sₘ
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<VAR>Algebra S Sₘ<VAR>i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>hRS : Function.Injective ⇑(algebraMap R S)<GOAL>Function.Injective ⇑(algebraMap Rₘ Sₘ)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>p : S[X]<VAR>i : ℕ<VAR>h : p.coeff i = 0<GOAL>IsLocalization.coeffIntegerNormalization M p i = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>p : S[X]<VAR>i : ℕ<VAR>h : IsLocalization.coeffIntegerNormalization M p i ≠ 0<GOAL>i ∈ p.support
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>p : S[X]<VAR>i : ℕ<GOAL>(IsLocalization.integerNormalization M p).coeff i = IsLocalization.coeffIntegerNormalization M p i
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>p : S[X]<GOAL>∃ b, ∀ (i : ℕ), (algebraMap R S) ((IsLocalization.integerNormalization M p).coeff i) = ↑b • p.coeff i
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>p : S[X]<GOAL>∃ b, Polynomial.map (algebraMap R S) (IsLocalization.integerNormalization M p) = ↑b • p
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>R' : Type u_4<VAR>CommRing R'<VAR>g : S →+* R'<VAR>p : S[X]<VAR>x : R'<VAR>hx : Polynomial.eval₂ g x p = 0<GOAL>Polynomial.eval₂ (g.comp (algebraMap R S)) x (IsLocalization.integerNormalization M p) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>R' : Type u_4<VAR>CommRing R'<VAR>Algebra R R'<VAR>Algebra S R'<VAR>IsScalarTower R S R'<VAR>p : S[X]<VAR>x : R'<VAR>hx : (Polynomial.aeval x) p = 0<GOAL>(Polynomial.aeval x) (IsLocalization.integerNormalization M p) = 0
<VAR>A : Type u_4<VAR>K : Type u_5<VAR>CommRing A<VAR>IsDomain A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>p : K[X]<GOAL>IsLocalization.integerNormalization (nonZeroDivisors A) p = 0 ↔ p = 0
<VAR>A : Type u_4<VAR>K : Type u_5<VAR>C : Type u_6<VAR>CommRing A<VAR>IsDomain A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>CommRing C<VAR>Algebra A C<VAR>Algebra K C<VAR>IsScalarTower A K C<VAR>x : C<GOAL>IsAlgebraic A x ↔ IsAlgebraic K x
<VAR>A : Type u_4<VAR>K : Type u_5<VAR>C : Type u_6<VAR>CommRing A<VAR>IsDomain A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>CommRing C<VAR>Algebra A C<VAR>Algebra K C<VAR>IsScalarTower A K C<GOAL>Algebra.IsAlgebraic A C ↔ Algebra.IsAlgebraic K C
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>hf : Polynomial.eval₂ f x p = 0<VAR>M : Submonoid R<VAR>hM : p.leadingCoeff ∈ M<VAR>Rₘ : Type u_8<VAR>Sₘ : Type u_9<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<VAR>Algebra S Sₘ<VAR>IsLocalization (Submonoid.map f M) Sₘ<GOAL>(IsLocalization.map Sₘ f ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<VAR>Algebra S Sₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>x : S<VAR>p : R[X]<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hM : p.leadingCoeff ∈ M<GOAL>(IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<VAR>Algebra S Sₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>Algebra.IsIntegral R S<GOAL>(IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegral
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : f.IsIntegral<VAR>M : Submonoid R<GOAL>(IsLocalization.map (Localization (Submonoid.map (↑f) M)) f ⋯).IsIntegral
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>Rₘ : Type u_4<VAR>CommRing Rₘ<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<VAR>p : Rₘ[X]<VAR>hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range<GOAL>p.scaleRoots ((algebraMap R Rₘ) ↑(IsLocalization.commonDenom M p.support p.coeff)) ∈ Polynomial.lifts (algebraMap R Rₘ)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Rₘ : Type u_4<VAR>CommRing Rₘ<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<VAR>Algebra Rₘ S<VAR>IsScalarTower R Rₘ S<VAR>x : S<VAR>hx : IsIntegral Rₘ x<GOAL>∃ m, IsIntegral R (m • x)
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>L : Type u_6<VAR>Field L<VAR>Algebra A L<VAR>C : Type u_7<VAR>CommRing C<VAR>IsDomain C<VAR>Algebra C L<VAR>IsIntegralClosure C A L<VAR>Algebra A C<VAR>IsScalarTower A C L<VAR>Algebra.IsAlgebraic A L<VAR>inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0<GOAL>IsFractionRing C L
<VAR>A : Type u_4<VAR>K : Type u_5<VAR>CommRing A<VAR>IsDomain A<VAR>L : Type u_6<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>Algebra A L<VAR>IsFractionRing A K<VAR>C : Type u_7<VAR>CommRing C<VAR>IsDomain C<VAR>Algebra C L<VAR>IsIntegralClosure C A L<VAR>Algebra A C<VAR>IsScalarTower A C L<VAR>Algebra K L<VAR>IsScalarTower A K L<VAR>FiniteDimensional K L<GOAL>IsFractionRing C L
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>L : Type u_6<VAR>Field L<VAR>Algebra A L<VAR>Algebra.IsAlgebraic A L<VAR>inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0<GOAL>IsFractionRing (↥(integralClosure A L)) L
<VAR>A : Type u_4<VAR>K : Type u_5<VAR>CommRing A<VAR>IsDomain A<VAR>L : Type u_6<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>Algebra A L<VAR>Algebra K L<VAR>IsScalarTower A K L<VAR>FiniteDimensional K L<GOAL>IsFractionRing (↥(integralClosure A L)) L
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>K : Type u_5<VAR>Field K<VAR>IsDomain R<VAR>IsDomain S<VAR>Algebra R K<VAR>Algebra S K<VAR>NoZeroSMulDivisors R K<VAR>IsFractionRing S K<VAR>IsScalarTower R S K<GOAL>Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>K : Type u_5<VAR>L : Type u_6<VAR>IsDomain R<VAR>IsDomain S<VAR>Field K<VAR>Field L<VAR>Algebra R K<VAR>Algebra R L<VAR>Algebra S L<VAR>IsIntegralClosure S R L<VAR>IsFractionRing S L<VAR>Algebra K L<VAR>IsScalarTower R S L<VAR>IsScalarTower R K L<VAR>a : S<VAR>b : Set S<VAR>Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)<GOAL>↑(Ideal.span {(algebraMap S L) a}) ⊆ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
<VAR>R : Type u_6<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_7<VAR>CommRing S<VAR>Nontrivial R<VAR>Algebra R S<VAR>IsLocalization M S<GOAL>Algebra.IsAlgebraic R S
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>K : Type u_8<VAR>L : Type u_9<VAR>CommRing R<VAR>CommRing S<VAR>Field K<VAR>CommRing L<VAR>Algebra R S<VAR>Algebra R K<VAR>Algebra R L<VAR>Algebra S L<VAR>Algebra K L<VAR>IsScalarTower R S L<VAR>IsScalarTower R K L<VAR>IsFractionRing S L<VAR>Algebra.IsIntegral R S<GOAL>Algebra.IsAlgebraic K L
<VAR>R : Type u<VAR>CommSemiring R<VAR>self : PrimeSpectrum R<GOAL>self.asIdeal.IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>x : PrimeSpectrum R<GOAL>((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal = x.asIdeal.prod ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>x : PrimeSpectrum S<GOAL>((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x)).asIdeal = ⊤.prod x.asIdeal
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : PrimeSpectrum R<VAR>s : Set R<GOAL>x ∈ PrimeSpectrum.zeroLocus s ↔ s ⊆ ↑x.asIdeal
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set R<GOAL>PrimeSpectrum.zeroLocus ↑(Ideal.span s) = PrimeSpectrum.zeroLocus s
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Set (PrimeSpectrum R)<GOAL>↑(PrimeSpectrum.vanishingIdeal t) = {f | ∀ x ∈ t, f ∈ x.asIdeal}
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Set (PrimeSpectrum R)<VAR>f : R<GOAL>f ∈ PrimeSpectrum.vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : PrimeSpectrum R<GOAL>PrimeSpectrum.vanishingIdeal {x} = x.asIdeal
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Set (PrimeSpectrum R)<VAR>I : Ideal R<GOAL>t ⊆ PrimeSpectrum.zeroLocus ↑I ↔ I ≤ PrimeSpectrum.vanishingIdeal t
<VAR>R : Type u<VAR>CommSemiring R<GOAL>GaloisConnection (fun I => PrimeSpectrum.zeroLocus ↑I) fun t => PrimeSpectrum.vanishingIdeal t
<VAR>R : Type u<VAR>CommSemiring R<GOAL>GaloisConnection (fun s => PrimeSpectrum.zeroLocus s) fun t => ↑(PrimeSpectrum.vanishingIdeal t)
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Set (PrimeSpectrum R)<VAR>s : Set R<GOAL>t ⊆ PrimeSpectrum.zeroLocus s ↔ s ⊆ ↑(PrimeSpectrum.vanishingIdeal t)
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set R<GOAL>s ⊆ ↑(PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus s))
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>I ≤ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I)
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I) = I.radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>PrimeSpectrum.zeroLocus ↑I.radical = PrimeSpectrum.zeroLocus ↑I
<VAR>R : Type u<VAR>CommSemiring R<VAR>t : Set (PrimeSpectrum R)<GOAL>t ⊆ PrimeSpectrum.zeroLocus ↑(PrimeSpectrum.vanishingIdeal t)
<VAR>R : Type u<VAR>CommSemiring R<VAR>s t : Set R<VAR>h : s ⊆ t<GOAL>PrimeSpectrum.zeroLocus t ⊆ PrimeSpectrum.zeroLocus s
<VAR>R : Type u<VAR>CommSemiring R<VAR>s t : Ideal R<VAR>h : s ≤ t<GOAL>PrimeSpectrum.zeroLocus ↑t ⊆ PrimeSpectrum.zeroLocus ↑s
<VAR>R : Type u<VAR>CommSemiring R<VAR>s t : Set (PrimeSpectrum R)<VAR>h : s ⊆ t<GOAL>PrimeSpectrum.vanishingIdeal t ≤ PrimeSpectrum.vanishingIdeal s
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>PrimeSpectrum.zeroLocus ↑I ⊆ PrimeSpectrum.zeroLocus ↑J ↔ J ≤ I.radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R<GOAL>PrimeSpectrum.zeroLocus {f} ⊆ PrimeSpectrum.zeroLocus {g} ↔ g ∈ (Ideal.span {f}).radical
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.zeroLocus ↑⊥ = Set.univ
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.zeroLocus {0} = Set.univ
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.zeroLocus ∅ = Set.univ
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.vanishingIdeal ∅ = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set R<VAR>h : 1 ∈ s<GOAL>PrimeSpectrum.zeroLocus s = ∅
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.zeroLocus {1} = ∅
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>PrimeSpectrum.zeroLocus ↑I = ∅ ↔ I = ⊤
<VAR>R : Type u<VAR>CommSemiring R<GOAL>PrimeSpectrum.zeroLocus Set.univ = ∅
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set (PrimeSpectrum R)<GOAL>PrimeSpectrum.vanishingIdeal s = ⊤ ↔ s = ∅
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set R<GOAL>PrimeSpectrum.zeroLocus s = ⊤ ↔ s ⊆ ↑(nilradical R)
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>PrimeSpectrum.zeroLocus ↑(I ⊔ J) = PrimeSpectrum.zeroLocus ↑I ∩ PrimeSpectrum.zeroLocus ↑J
<VAR>R : Type u<VAR>CommSemiring R<VAR>s s' : Set R<GOAL>PrimeSpectrum.zeroLocus (s ∪ s') = PrimeSpectrum.zeroLocus s ∩ PrimeSpectrum.zeroLocus s'
<VAR>R : Type u<VAR>CommSemiring R<VAR>t t' : Set (PrimeSpectrum R)<GOAL>PrimeSpectrum.vanishingIdeal (t ∪ t') = PrimeSpectrum.vanishingIdeal t ⊓ PrimeSpectrum.vanishingIdeal t'
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Sort u_1<VAR>I : ι → Ideal R<GOAL>PrimeSpectrum.zeroLocus ↑(⨆ i, I i) = ⋂ i, PrimeSpectrum.zeroLocus ↑(I i)
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Sort u_1<VAR>s : ι → Set R<GOAL>PrimeSpectrum.zeroLocus (⋃ i, s i) = ⋂ i, PrimeSpectrum.zeroLocus (s i)
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>s : (i : ι) → κ i → Set R<GOAL>PrimeSpectrum.zeroLocus (⋃ i, ⋃ j, s i j) = ⋂ i, ⋂ j, PrimeSpectrum.zeroLocus (s i j)
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set (Set R)<GOAL>PrimeSpectrum.zeroLocus (⋃ s' ∈ s, s') = ⋂ s' ∈ s, PrimeSpectrum.zeroLocus s'
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Sort u_1<VAR>t : ι → Set (PrimeSpectrum R)<GOAL>PrimeSpectrum.vanishingIdeal (⋃ i, t i) = ⨅ i, PrimeSpectrum.vanishingIdeal (t i)
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>PrimeSpectrum.zeroLocus ↑(I ⊓ J) = PrimeSpectrum.zeroLocus ↑I ∪ PrimeSpectrum.zeroLocus ↑J
<VAR>R : Type u<VAR>CommSemiring R<VAR>s s' : Set R<GOAL>PrimeSpectrum.zeroLocus s ∪ PrimeSpectrum.zeroLocus s' = PrimeSpectrum.zeroLocus ↑(Ideal.span s ⊓ Ideal.span s')
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>PrimeSpectrum.zeroLocus ↑(I * J) = PrimeSpectrum.zeroLocus ↑I ∪ PrimeSpectrum.zeroLocus ↑J
<VAR>R : Type u<VAR>CommSemiring R<VAR>f g : R<GOAL>PrimeSpectrum.zeroLocus {f * g} = PrimeSpectrum.zeroLocus {f} ∪ PrimeSpectrum.zeroLocus {g}
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>PrimeSpectrum.zeroLocus ↑(I ^ n) = PrimeSpectrum.zeroLocus ↑I
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>PrimeSpectrum.zeroLocus {f ^ n} = PrimeSpectrum.zeroLocus {f}
<VAR>R : Type u<VAR>CommSemiring R<VAR>t t' : Set (PrimeSpectrum R)<GOAL>PrimeSpectrum.vanishingIdeal t ⊔ PrimeSpectrum.vanishingIdeal t' ≤ PrimeSpectrum.vanishingIdeal (t ∩ t')
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R<VAR>I : PrimeSpectrum R<GOAL>I ∈ (PrimeSpectrum.zeroLocus {f})ᶜ ↔ f ∉ I.asIdeal
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : PrimeSpectrum R<GOAL>x.asIdeal ≤ y.asIdeal ↔ x ≤ y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : PrimeSpectrum R<GOAL>x.asIdeal < y.asIdeal ↔ x < y
<VAR>R : Type u<VAR>CommRing R<VAR>IsNoetherianRing R<VAR>I : Ideal R<GOAL>∃ Z, (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I
<VAR>A : Type u<VAR>CommRing A<VAR>IsDomain A<VAR>IsNoetherianRing A<VAR>h_fA : ¬IsField A<VAR>I : Ideal A<VAR>h_nzI : I ≠ ⊥<GOAL>∃ Z, (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ (Multiset.map PrimeSpectrum.asIdeal Z).prod ≠ ⊥
<VAR>R : Type u_1<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<VAR>x y : Rᵐᵒᵖ<GOAL>c.op x y ↔ c (MulOpposite.unop y) (MulOpposite.unop x)
<VAR>R : Type u_1<VAR>Add R<VAR>Mul R<VAR>c : RingCon Rᵐᵒᵖ<VAR>x y : R<GOAL>c.unop x y ↔ c (MulOpposite.op y) (MulOpposite.op x)
<VAR>R : Type u_1<VAR>Add R<VAR>Mul R<VAR>c : RingCon Rᵐᵒᵖ<GOAL>(RelIso.symm RingCon.opOrderIso) c = c.unop
<VAR>R : Type u_1<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<GOAL>RingCon.opOrderIso c = c.op
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>b : A<VAR>a : R[X]<GOAL>((PolyEquivTensor.toFunBilinear R A) b) a = b • (Polynomial.aeval Polynomial.X) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<VAR>p : R[X]<GOAL>((PolyEquivTensor.toFunBilinear R A) a) p = p.sum fun n r => (Polynomial.monomial n) (a * (algebraMap R A) r)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<VAR>p : R[X]<GOAL>(PolyEquivTensor.toFunLinear R A) (a ⊗ₜ[R] p) = ((PolyEquivTensor.toFunBilinear R A) a) p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p : R[X]<VAR>k : ℕ<VAR>h : Decidable ¬p.coeff k = 0<VAR>a : A<GOAL>(if ¬p.coeff k = 0 then a * (algebraMap R A) (p.coeff k) else 0) = a * (algebraMap R A) (p.coeff k)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>k : ℕ<VAR>a₁ a₂ : A<VAR>p₁ p₂ : R[X]<GOAL>a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) = ∑ x ∈ Finset.antidiagonal k, a₁ * (algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff x.2))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a₁ a₂ : A<VAR>p₁ p₂ : R[X]<GOAL>(PolyEquivTensor.toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = (PolyEquivTensor.toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * (PolyEquivTensor.toFunLinear R A) (a₂ ⊗ₜ[R] p₂)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>(PolyEquivTensor.toFunLinear R A) (1 ⊗ₜ[R] 1) = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<VAR>p : R[X]<GOAL>(PolyEquivTensor.toFunAlgHom R A) (a ⊗ₜ[R] p) = p.sum fun n r => (Polynomial.monomial n) (a * (algebraMap R A) r)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p q : A[X]<GOAL>PolyEquivTensor.invFun R A (p + q) = PolyEquivTensor.invFun R A p + PolyEquivTensor.invFun R A q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>n : ℕ<VAR>a : A<GOAL>PolyEquivTensor.invFun R A ((Polynomial.monomial n) a) = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] Polynomial.X ^ n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A ⊗[R] R[X]<GOAL>PolyEquivTensor.invFun R A ((PolyEquivTensor.toFunAlgHom R A) x) = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A[X]<GOAL>(PolyEquivTensor.toFunAlgHom R A) (PolyEquivTensor.invFun R A x) = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p : A[X]<GOAL>(polyEquivTensor R A) p = Polynomial.eval₂ (↑Algebra.TensorProduct.includeLeft) (1 ⊗ₜ[R] Polynomial.X) p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<VAR>p : R[X]<GOAL>(polyEquivTensor R A).symm (a ⊗ₜ[R] p) = p.sum fun n r => (Polynomial.monomial n) (a * (algebraMap R A) r)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>matPolyEquiv.symm (Polynomial.C M) = M.map ⇑Polynomial.C
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>matPolyEquiv (M.map ⇑Polynomial.C) = Polynomial.C M
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<GOAL>matPolyEquiv.symm Polynomial.X = Matrix.diagonal fun x => Polynomial.X
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<GOAL>matPolyEquiv (Matrix.diagonal fun x => Polynomial.X) = Polynomial.X
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>i j : n<VAR>k : ℕ<VAR>x : R<GOAL>matPolyEquiv (Matrix.stdBasisMatrix i j ((Polynomial.monomial k) x)) = (Polynomial.monomial k) (Matrix.stdBasisMatrix i j x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>i j : n<VAR>p : R[X]<VAR>k : ℕ<GOAL>(matPolyEquiv (Matrix.stdBasisMatrix i j p)).coeff k = Matrix.stdBasisMatrix i j (p.coeff k)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>m : Matrix n n R[X]<VAR>k : ℕ<VAR>i j : n<GOAL>(matPolyEquiv m).coeff k i j = (m i j).coeff k
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>p : (Matrix n n R)[X]<VAR>i j : n<VAR>k : ℕ<GOAL>(matPolyEquiv.symm p i j).coeff k = p.coeff k i j
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>p : R[X]<GOAL>matPolyEquiv (p • 1) = Polynomial.map (algebraMap R (Matrix n n R)) p
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>p : R[X]<VAR>M : Matrix n n R[X]<GOAL>matPolyEquiv (p • M) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv M
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>m : Matrix n n R[X]<VAR>i j : n<GOAL>(m i j).support ⊆ (matPolyEquiv m).support
<VAR>R : Type u<VAR>CommRing R<VAR>self : MaximalSpectrum R<GOAL>self.asIdeal.IsMaximal
<VAR>R : Type u<VAR>CommRing R<GOAL>Function.Injective MaximalSpectrum.toPrimeSpectrum
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>σ : Type u_2<VAR>f : σ → R<VAR>s : Finset σ<VAR>n : ℕ<GOAL>(Multiset.map f s.val).esymm n = ∑ t ∈ Finset.powersetCard n s, t.prod f
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p ∈ MvPolynomial.symmetricSubalgebra σ R ↔ p.IsSymmetric
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>r : R<GOAL>(MvPolynomial.C r).IsSymmetric
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>MvPolynomial.IsSymmetric 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>MvPolynomial.IsSymmetric 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ ψ : MvPolynomial σ R<VAR>hφ : φ.IsSymmetric<VAR>hψ : ψ.IsSymmetric<GOAL>(φ + ψ).IsSymmetric
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ ψ : MvPolynomial σ R<VAR>hφ : φ.IsSymmetric<VAR>hψ : ψ.IsSymmetric<GOAL>(φ * ψ).IsSymmetric
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>r : R<VAR>hφ : φ.IsSymmetric<GOAL>(r • φ).IsSymmetric
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>φ : MvPolynomial σ R<VAR>hφ : φ.IsSymmetric<VAR>f : R →+* S<GOAL>((MvPolynomial.map f) φ).IsSymmetric
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>hφ : φ.IsSymmetric<VAR>e : σ ≃ τ<GOAL>((MvPolynomial.rename ⇑e) φ).IsSymmetric
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>e : σ ≃ τ<GOAL>((MvPolynomial.rename ⇑e) φ).IsSymmetric ↔ φ.IsSymmetric
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>φ : MvPolynomial σ R<VAR>hφ : φ.IsSymmetric<GOAL>(-φ).IsSymmetric
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>φ ψ : MvPolynomial σ R<VAR>hφ : φ.IsSymmetric<VAR>hψ : ψ.IsSymmetric<GOAL>(φ - ψ).IsSymmetric
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>CommSemiring R<VAR>e : σ ≃ τ<VAR>a : ↥(MvPolynomial.symmetricSubalgebra σ R)<GOAL>↑((MvPolynomial.renameSymmetricSubalgebra e) a) = (MvPolynomial.rename ⇑e) ↑a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>CommSemiring R<VAR>e : σ ≃ τ<VAR>a : ↥(MvPolynomial.symmetricSubalgebra τ R)<GOAL>↑((MvPolynomial.renameSymmetricSubalgebra e).symm a) = (MvPolynomial.rename ⇑e.symm) ↑a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<GOAL>MvPolynomial.esymm σ R = (Multiset.map MvPolynomial.X Finset.univ.val).esymm
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Fintype σ<VAR>Algebra R S<VAR>f : σ → S<VAR>n : ℕ<GOAL>(MvPolynomial.aeval f) (MvPolynomial.esymm σ R n) = (Multiset.map f Finset.univ.val).esymm n
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<VAR>n : ℕ<GOAL>MvPolynomial.esymm σ R n = ∑ t : { s // s.card = n }, ∏ i ∈ ↑t, MvPolynomial.X i
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<VAR>n : ℕ<GOAL>MvPolynomial.esymm σ R n = ∑ t ∈ Finset.powersetCard n Finset.univ, (MvPolynomial.monomial (∑ i ∈ t, Finsupp.single i 1)) 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<GOAL>MvPolynomial.esymm σ R 0 = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Fintype σ<VAR>n : ℕ<VAR>f : R →+* S<GOAL>(MvPolynomial.map f) (MvPolynomial.esymm σ R n) = MvPolynomial.esymm σ S n
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>CommSemiring R<VAR>Fintype σ<VAR>Fintype τ<VAR>n : ℕ<VAR>e : σ ≃ τ<GOAL>(MvPolynomial.rename ⇑e) (MvPolynomial.esymm σ R n) = MvPolynomial.esymm τ R n
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<VAR>n : ℕ<GOAL>(MvPolynomial.esymm σ R n).IsSymmetric