ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<GOAL>Subsingleton (OreLocalization S R) ↔ 0 ∈ S
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<GOAL>Nontrivial (OreLocalization S R) ↔ 0 ∉ S
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>Nontrivial R<VAR>hS : S ≤ nonZeroDivisors R<GOAL>Nontrivial (OreLocalization S R)
<VAR>R : Type u_1<VAR>Ring R<VAR>Nontrivial R<VAR>OreLocalization.OreSet (nonZeroDivisors R)<VAR>NoZeroDivisors R<VAR>r : R<VAR>s : ↥(nonZeroDivisors R)<GOAL>(r /ₒ s)⁻¹ = if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩
<VAR>R : Type u_1<VAR>Ring R<VAR>Nontrivial R<VAR>OreLocalization.OreSet (nonZeroDivisors R)<VAR>NoZeroDivisors R<VAR>x : OreLocalization (nonZeroDivisors R) R<VAR>h : x ≠ 0<GOAL>x * x⁻¹ = 1
<VAR>R : Type u_1<VAR>Ring R<VAR>Nontrivial R<VAR>OreLocalization.OreSet (nonZeroDivisors R)<VAR>NoZeroDivisors R<GOAL>0⁻¹ = 0
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>IsDomain R<VAR>h : f.degree ≠ 0<GOAL>Nontrivial (AdjoinRoot f)
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>C : AdjoinRoot f → Prop<VAR>x : AdjoinRoot f<VAR>ih : ∀ (p : R[X]), C ((AdjoinRoot.mk f) p)<GOAL>C x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>DistribSMul S R<VAR>IsScalarTower S R R<VAR>a : S<VAR>x : R[X]<GOAL>a • (AdjoinRoot.mk f) x = (AdjoinRoot.mk f) (a • x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>DistribSMul S R<VAR>IsScalarTower S R R<VAR>a : S<VAR>x : R<GOAL>a • (AdjoinRoot.of f) x = (AdjoinRoot.of f) (a • x)
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<GOAL>algebraMap R (AdjoinRoot f) = AdjoinRoot.of f
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>CommSemiring S<VAR>Algebra S R<GOAL>algebraMap S (AdjoinRoot f) = (AdjoinRoot.of f).comp (algebraMap S R)
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<GOAL>Algebra.FiniteType R (AdjoinRoot f)
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<GOAL>Algebra.FinitePresentation R (AdjoinRoot f)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>Semiring S<VAR>Algebra R S<VAR>g₁ g₂ : AdjoinRoot f →ₐ[R] S<VAR>h : g₁ (AdjoinRoot.root f) = g₂ (AdjoinRoot.root f)<GOAL>g₁ = g₂
<VAR>R : Type u<VAR>CommRing R<VAR>f g h : R[X]<GOAL>(AdjoinRoot.mk f) g = (AdjoinRoot.mk f) h ↔ f ∣ g - h
<VAR>R : Type u<VAR>CommRing R<VAR>f g : R[X]<GOAL>(AdjoinRoot.mk f) g = 0 ↔ f ∣ g
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<GOAL>(AdjoinRoot.mk f) f = 0
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>x : R<GOAL>(AdjoinRoot.mk f) (Polynomial.C x) = (AdjoinRoot.of f) x
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<GOAL>(AdjoinRoot.mk f) Polynomial.X = AdjoinRoot.root f
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : R[X]<VAR>h0 : g ≠ 0<VAR>hd : g.degree < f.degree<GOAL>(AdjoinRoot.mk f) g ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : R[X]<VAR>h0 : g ≠ 0<VAR>hd : g.natDegree < f.natDegree<GOAL>(AdjoinRoot.mk f) g ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>p : R[X]<GOAL>(Polynomial.aeval (AdjoinRoot.root f)) p = (AdjoinRoot.mk f) p
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<GOAL>Algebra.adjoin R {AdjoinRoot.root f} = ⊤
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<GOAL>Polynomial.eval₂ (AdjoinRoot.of f) (AdjoinRoot.root f) f = 0
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<GOAL>(Polynomial.map (AdjoinRoot.of f) f).IsRoot (AdjoinRoot.root f)
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>hf : f ≠ 0<GOAL>IsAlgebraic R (AdjoinRoot.root f)
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>IsDomain R<VAR>hf : f.degree ≠ 0<GOAL>Function.Injective ⇑(AdjoinRoot.of f)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h : Polynomial.eval₂ i a f = 0<VAR>g : R[X]<GOAL>(AdjoinRoot.lift i a h) ((AdjoinRoot.mk f) g) = Polynomial.eval₂ i a g
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h : Polynomial.eval₂ i a f = 0<GOAL>(AdjoinRoot.lift i a h) (AdjoinRoot.root f) = a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h : Polynomial.eval₂ i a f = 0<VAR>x : R<GOAL>(AdjoinRoot.lift i a h) ((AdjoinRoot.of f) x) = i x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h : Polynomial.eval₂ i a f = 0<GOAL>(AdjoinRoot.lift i a h).comp (AdjoinRoot.of f) = i
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>hfx : (Polynomial.aeval x) f = 0<GOAL>↑(AdjoinRoot.liftHom f x hfx) = AdjoinRoot.lift (algebraMap R S) x hfx
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>CommRing S<VAR>Algebra R S<VAR>ϕ : AdjoinRoot f →ₐ[R] S<GOAL>(Polynomial.aeval (ϕ (AdjoinRoot.root f))) f = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>ϕ : AdjoinRoot f →ₐ[R] S<GOAL>AdjoinRoot.liftHom f (ϕ (AdjoinRoot.root f)) ⋯ = ϕ
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>CommRing S<VAR>a : S<VAR>Algebra R S<VAR>hfx : (Polynomial.aeval a) f = 0<VAR>g : R[X]<GOAL>(AdjoinRoot.liftHom f a hfx) ((AdjoinRoot.mk f) g) = (Polynomial.aeval a) g
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>CommRing S<VAR>a : S<VAR>Algebra R S<VAR>hfx : (Polynomial.aeval a) f = 0<GOAL>(AdjoinRoot.liftHom f a hfx) (AdjoinRoot.root f) = a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>f : R[X]<VAR>CommRing S<VAR>a : S<VAR>Algebra R S<VAR>hfx : (Polynomial.aeval a) f = 0<VAR>x : R<GOAL>(AdjoinRoot.liftHom f a hfx) ((AdjoinRoot.of f) x) = (algebraMap R S) x
<VAR>R : Type u<VAR>CommRing R<VAR>r : R<GOAL>(AdjoinRoot.of (Polynomial.C r * Polynomial.X - 1)) r * AdjoinRoot.root (Polynomial.C r * Polynomial.X - 1) = 1
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type u_1<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<GOAL>Subsingleton (AdjoinRoot (Polynomial.C r * Polynomial.X - 1) →ₐ[R] S)
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>hf : Prime f<GOAL>IsDomain (AdjoinRoot f)
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>IsDomain R<VAR>hf : Prime f<VAR>hf' : f.degree ≠ 0<GOAL>NoZeroSMulDivisors R (AdjoinRoot f)
<VAR>K : Type w<VAR>Field K<VAR>f : K[X]<VAR>h : f.degree ≠ 0<GOAL>Function.Injective ⇑(AdjoinRoot.of f)
<VAR>K : Type w<VAR>Field K<VAR>f : K[X]<VAR>Fact (Irreducible f)<GOAL>Function.Injective ⇑(AdjoinRoot.of f)
<VAR>K : Type w<VAR>Field K<VAR>f : K[X]<VAR>Fact (Irreducible f)<GOAL>(Polynomial.X - Polynomial.C (AdjoinRoot.root f)) * (Polynomial.map (AdjoinRoot.of f) f / (Polynomial.X - Polynomial.C (AdjoinRoot.root f))) = Polynomial.map (AdjoinRoot.of f) f
<VAR>R : Type u<VAR>CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<GOAL>IsIntegral R (AdjoinRoot.root g)
<VAR>R : Type u<VAR>CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<VAR>f : R[X]<GOAL>(AdjoinRoot.modByMonicHom hg) ((AdjoinRoot.mk g) f) = f %ₘ g
<VAR>R : Type u<VAR>CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<GOAL>Function.LeftInverse ⇑(AdjoinRoot.mk g) ⇑(AdjoinRoot.modByMonicHom hg)
<VAR>R : Type u<VAR>CommRing R<VAR>g : R[X]<GOAL>Function.Surjective ⇑(AdjoinRoot.mk g)
<VAR>R : Type u<VAR>CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<VAR>c : Fin g.natDegree →₀ R<GOAL>(AdjoinRoot.powerBasisAux' hg).repr.symm c = (AdjoinRoot.mk g) (∑ i : Fin g.natDegree, (Polynomial.monomial ↑i) (c i))
<VAR>R : Type u<VAR>CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<VAR>f : AdjoinRoot g<VAR>i : Fin g.natDegree<GOAL>((AdjoinRoot.powerBasisAux' hg).repr f) i = ((AdjoinRoot.modByMonicHom hg) f).coeff ↑i
<VAR>R : Type u<VAR>CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<GOAL>(AdjoinRoot.powerBasis' hg).dim = g.natDegree
<VAR>R : Type u<VAR>CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<GOAL>(AdjoinRoot.powerBasis' hg).gen = AdjoinRoot.root g
<VAR>K : Type w<VAR>Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<GOAL>IsIntegral K (AdjoinRoot.root f)
<VAR>K : Type w<VAR>Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<GOAL>minpoly K (AdjoinRoot.root f) = f * Polynomial.C f.leadingCoeff⁻¹
<VAR>K : Type w<VAR>Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<GOAL>(AdjoinRoot.powerBasis hf).dim = f.natDegree
<VAR>K : Type w<VAR>Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<GOAL>(AdjoinRoot.powerBasis hf).gen = AdjoinRoot.root f
<VAR>K : Type w<VAR>Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<GOAL>minpoly K (AdjoinRoot.powerBasis hf).gen = f * Polynomial.C f.leadingCoeff⁻¹
<VAR>K : Type w<VAR>Field K<VAR>f : K[X]<VAR>hf : f.Monic<VAR>hf' : f ≠ 0 := ⋯<GOAL>minpoly K (AdjoinRoot.powerBasis hf').gen = f
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<GOAL>∀ (a : R[X] ⧸ Submodule.toAddSubgroup (Ideal.span {minpoly R x})), (AdjoinRoot.Minpoly.toAdjoin R x) a = (QuotientAddGroup.lift (Submodule.toAddSubgroup (Ideal.span {minpoly R x})) ↑(Polynomial.eval₂RingHom (algebraMap R ↥(Algebra.adjoin R {x})) ⟨x, ⋯⟩) ⋯) a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>a : AdjoinRoot (minpoly R x)<GOAL>(AdjoinRoot.Minpoly.toAdjoin R x) a = (AdjoinRoot.liftHom (minpoly R x) ⟨x, ⋯⟩ ⋯) a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<GOAL>(AdjoinRoot.Minpoly.toAdjoin R x) ((AdjoinRoot.mk (minpoly R x)) Polynomial.X) = ⟨x, ⋯⟩
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<GOAL>Function.Surjective ⇑(AdjoinRoot.Minpoly.toAdjoin R x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>g : R[X]<VAR>pb : PowerBasis R S<VAR>h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0<VAR>h₂ : (Polynomial.aeval pb.gen) g = 0<GOAL>⇑(AdjoinRoot.equiv' g pb h₁ h₂).symm = ⇑(pb.lift (AdjoinRoot.root g) h₁)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>g : R[X]<VAR>pb : PowerBasis R S<VAR>h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0<VAR>h₂ : (Polynomial.aeval pb.gen) g = 0<GOAL>⇑(AdjoinRoot.equiv' g pb h₁ h₂) = ⇑(AdjoinRoot.liftHom g pb.gen h₂)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>g : R[X]<VAR>pb : PowerBasis R S<VAR>h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0<VAR>h₂ : (Polynomial.aeval pb.gen) g = 0<GOAL>↑(AdjoinRoot.equiv' g pb h₁ h₂) = AdjoinRoot.liftHom g pb.gen h₂
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>g : R[X]<VAR>pb : PowerBasis R S<VAR>h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0<VAR>h₂ : (Polynomial.aeval pb.gen) g = 0<GOAL>↑(AdjoinRoot.equiv' g pb h₁ h₂).symm = pb.lift (AdjoinRoot.root g) h₁
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>f : R[X]<VAR>x : AdjoinRoot f<GOAL>(AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk I f) ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) x) = (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) x
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>f : R[X]<VAR>x : AdjoinRoot f<GOAL>(AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk I f).symm ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) x) = (Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) x
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>f p : R[X]<GOAL>(AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) ((AdjoinRoot.mk f) p)) = (DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>f p : R[X]<GOAL>(AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f).symm ((DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p) = (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) ((AdjoinRoot.mk f) p)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>f p : R[X]<GOAL>(AdjoinRoot.Polynomial.quotQuotEquivComm I f) ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) = (Ideal.Quotient.mk (Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f})) ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) p)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>f p : R[X]<GOAL>(AdjoinRoot.Polynomial.quotQuotEquivComm I f).symm ((Ideal.Quotient.mk (Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f})) ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) p)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>f p : R[X]<GOAL>(AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f) ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) p)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>f p : R[X]<GOAL>(AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f).symm ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) = (Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) p)
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>I : Ideal R<VAR>a : AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.of f) I<GOAL>(AdjoinRoot.quotEquivQuotMap f I) a = (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f) a
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>I : Ideal R<VAR>a : (R ⧸ I)[X] ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}<GOAL>(AdjoinRoot.quotEquivQuotMap f I).symm a = (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f).symm a
<VAR>R : Type u<VAR>CommRing R<VAR>f g : R[X]<VAR>I : Ideal R<GOAL>(AdjoinRoot.quotEquivQuotMap f I) ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) g)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)
<VAR>R : Type u<VAR>CommRing R<VAR>f g : R[X]<VAR>I : Ideal R<GOAL>(AdjoinRoot.quotEquivQuotMap f I).symm ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)) = (Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) g)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>pb : PowerBasis R S<VAR>I : Ideal R<GOAL>∀ (a : (R ⧸ I)[X] ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}), (pb.quotientEquivQuotientMinpolyMap I).symm a = (↑↑(AlgEquiv.ofRingEquiv ⋯)).symm ((↑↑(AdjoinRoot.quotEquivQuotMap (minpoly R pb.gen) I)).symm a)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>pb : PowerBasis R S<VAR>I : Ideal R<GOAL>∀ (a : S ⧸ Ideal.map (algebraMap R S) I), (pb.quotientEquivQuotientMinpolyMap I) a = (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I (minpoly R pb.gen)) ((Ideal.quotientMap (Ideal.map (AdjoinRoot.of (minpoly R pb.gen)) I) ↑(↑(AdjoinRoot.equiv' (minpoly R pb.gen) pb ⋯ ⋯)).symm ⋯) a)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>pb : PowerBasis R S<VAR>I : Ideal R<VAR>g : R[X]<GOAL>(pb.quotientEquivQuotientMinpolyMap I) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((Polynomial.aeval pb.gen) g)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})) (Polynomial.map (Ideal.Quotient.mk I) g)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>pb : PowerBasis R S<VAR>I : Ideal R<VAR>g : R[X]<GOAL>(pb.quotientEquivQuotientMinpolyMap I).symm ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})) (Polynomial.map (Ideal.Quotient.mk I) g)) = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((Polynomial.aeval pb.gen) g)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommRing K<VAR>IsDomain K<VAR>Field L<VAR>Algebra K L<VAR>Algebra.IsIntegral K L<VAR>f : L[X]<VAR>hf : Irreducible f<GOAL>∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>minimalPrimes R = minimals (fun x x_1 => x ≤ x_1) (setOf Ideal.IsPrime)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>J.IsPrime<VAR>e : I ≤ J<GOAL>∃ p ∈ I.minimalPrimes, p ≤ J
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>I.radical.minimalPrimes = I.minimalPrimes
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>sInf I.minimalPrimes = I.radical
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<GOAL>∃ p', p'.IsPrime ∧ Ideal.comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (Ideal.comap f I).minimalPrimes<GOAL>∃ p', p'.IsPrime ∧ I ≤ p' ∧ Ideal.comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (Ideal.comap f I).minimalPrimes<GOAL>∃ p' ∈ I.minimalPrimes, Ideal.comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<VAR>h : J ∈ I.minimalPrimes<GOAL>Ideal.comap f J ∈ (Ideal.comap f I).minimalPrimes
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal S<GOAL>(Ideal.comap f I).minimalPrimes = Ideal.comap f '' I.minimalPrimes
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<GOAL>I.minimalPrimes = Ideal.comap (Ideal.Quotient.mk I) '' minimalPrimes (R ⧸ I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>hI : I.IsPrimary<GOAL>I.minimalPrimes = {I.radical}
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>I.IsPrime<GOAL>I.minimalPrimes = {I}
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hMin : I ∈ minimalPrimes R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>IsLocalization.AtPrime S I<VAR>J K : Ideal S<VAR>J.IsPrime<VAR>K.IsPrime<GOAL>J = K
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hMin : I ∈ minimalPrimes R<VAR>J : Ideal (Localization I.primeCompl)<VAR>J.IsPrime<GOAL>J = LocalRing.maximalIdeal (Localization I.primeCompl)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hMin : I ∈ minimalPrimes R<VAR>x : Localization I.primeCompl<GOAL>IsNilpotent x ↔ x ∈ LocalRing.maximalIdeal (Localization I.primeCompl)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hMin : I ∈ minimalPrimes R<VAR>x : Localization I.primeCompl<GOAL>IsNilpotent x ↔ x ∈ nonunits (Localization I.primeCompl)
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>Pow R ℕ<VAR>self : BinomialRing R<VAR>r : R<VAR>n : ℕ<GOAL>n.factorial • BinomialRing.multichoose r n = (ascPochhammer ℕ n).smeval r
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>Pow R ℕ<VAR>self : BinomialRing R<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Function.Injective fun x => n • x
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Function.Injective fun x => n • x
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>r : R<VAR>n : ℕ<GOAL>BinomialRing.multichoose r n = Ring.multichoose r n
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>r : R<VAR>n : ℕ<GOAL>n.factorial • Ring.multichoose r n = (ascPochhammer ℕ n).smeval r
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>r : R<GOAL>Ring.multichoose r 0 = r ^ 0
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>MulOneClass R<VAR>NatPowAssoc R<VAR>r : R<GOAL>Ring.multichoose r 0 = 1
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>r : R<GOAL>Ring.multichoose r 1 = r ^ 1
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>MulOneClass R<VAR>NatPowAssoc R<VAR>r : R<GOAL>Ring.multichoose r 1 = r
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>BinomialRing R<VAR>k : ℕ<GOAL>Ring.multichoose 0 (k + 1) = 0
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>(ascPochhammer ℕ (k + 1)).smeval (r + 1) = (k + 1).factorial • Ring.multichoose (r + 1) k + (ascPochhammer ℕ (k + 1)).smeval r
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>Ring.multichoose (r + 1) (k + 1) = Ring.multichoose r (k + 1) + Ring.multichoose (r + 1) k
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>BinomialRing R<VAR>k : ℕ<GOAL>Ring.multichoose 1 k = 1
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>BinomialRing R<VAR>k : ℕ<GOAL>Ring.multichoose 2 k = ↑k + 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>NonAssocSemiring S<VAR>Pow S ℕ<VAR>Module R S<VAR>IsScalarTower R S S<VAR>NatPowAssoc S<VAR>x : S<VAR>n : ℕ<GOAL>(ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>n : ℕ<GOAL>(ascPochhammer ℕ n).smeval r = Polynomial.eval r (ascPochhammer R n)
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>r : R<VAR>n : ℕ<GOAL>(descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>n k : ℕ<GOAL>(descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>r : R<VAR>k : ℕ<GOAL>(ascPochhammer ℕ k).smeval (-r) = (-1) ^ k * (descPochhammer ℤ k).smeval r
<VAR>n : ℕ<GOAL>(ascPochhammer ℕ n).smeval (-↑n) = (-1) ^ n * ↑n.factorial
<VAR>n : ℕ<GOAL>(ascPochhammer ℕ (n + 1)).smeval (-↑n) = 0
<VAR>n k : ℕ<GOAL>(ascPochhammer ℕ (n + k + 1)).smeval (-↑n) = 0
<VAR>n k : ℕ<VAR>h : n < k<GOAL>(ascPochhammer ℕ k).smeval (-↑n) = 0
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>n k : ℕ<GOAL>(ascPochhammer ℕ k).smeval ↑n = ↑((ascPochhammer ℕ k).smeval n)
<VAR>n : ℕ<GOAL>Ring.multichoose (-↑n) n = (-1) ^ n
<VAR>n : ℕ<GOAL>Ring.multichoose (-↑n) (n + 1) = 0
<VAR>n k : ℕ<GOAL>Ring.multichoose (-↑n) (n + k + 1) = 0
<VAR>n k : ℕ<VAR>h : n < k<GOAL>Ring.multichoose (-↑n) k = 0
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>NatPowAssoc R<VAR>n : ℕ<GOAL>Ring.multichoose (-↑n) (n + 1) = 0
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>r : R<VAR>n : ℕ<GOAL>(ascPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval r
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>NatPowAssoc R<VAR>r : R<VAR>n : ℕ<GOAL>(descPochhammer ℤ n).smeval r = n.factorial • Ring.choose r n
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>NatPowAssoc R<VAR>n k : ℕ<GOAL>Ring.choose (↑n) k = ↑(n.choose k)
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>r : R<GOAL>Ring.choose r 0 = (r + 1) ^ 0
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>NatPowAssoc R<VAR>r : R<GOAL>Ring.choose r 0 = 1
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>BinomialRing R<VAR>n : ℕ<GOAL>Ring.choose 0 (n + 1) = 0
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>BinomialRing R<VAR>k : ℕ<VAR>h_pos : 0 < k<GOAL>Ring.choose 0 k = 0
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>BinomialRing R<VAR>k : ℕ<GOAL>Ring.choose 0 k = if k = 0 then 1 else 0
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>r : R<GOAL>Ring.choose r 1 = r ^ 1
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>NatPowAssoc R<VAR>r : R<GOAL>Ring.choose r 1 = r
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>r : R<VAR>k : ℕ<GOAL>(descPochhammer ℤ (k + 1)).smeval (r + 1) = (k + 1) • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ (k + 1)).smeval r
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>NatPowAssoc R<VAR>r : R<VAR>k : ℕ<GOAL>Ring.choose (r + 1) (k + 1) = Ring.choose r k + Ring.choose r (k + 1)
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>NatPowAssoc R<VAR>r : R<VAR>n k : ℕ<VAR>hkn : k ≤ n<GOAL>n.choose k • Ring.choose r n = Ring.choose r k * Ring.choose (r - ↑k) (n - k)