ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>m n a : ℕ<VAR>hmn : m ≤ n<VAR>x : R ⧸ I ^ n • ⊤<GOAL>(AdicCompletion.transitionMap I R hmn) (x ^ a) = (AdicCompletion.transitionMap I R hmn) x ^ a
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>n : ℕ<GOAL>↑1 n = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>n : ℕ<VAR>x y : AdicCompletion I R<GOAL>↑(x * y) n = ↑x n * ↑y n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>n : ℕ<VAR>x : AdicCompletion.AdicCauchySequence I R<GOAL>(AdicCompletion.evalₐ I n) ((AdicCompletion.mk I R) x) = (Ideal.Quotient.mk (I ^ n)) (↑x n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>n : ℕ<VAR>f g : AdicCompletion.AdicCauchySequence I R<GOAL>↑(f * g) n = ↑f n * ↑g n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>a : AdicCompletion.AdicCauchySequence I R<VAR>n : ℕ<GOAL>↑((AdicCompletion.mkₐ I) a) n = (Ideal.Quotient.mk (I ^ n • ⊤)) (↑a n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>n : ℕ<VAR>x : AdicCompletion.AdicCauchySequence I R<GOAL>(AdicCompletion.evalₐ I n) ((AdicCompletion.mkₐ I) x) = (Ideal.Quotient.mk (I ^ n)) (↑x n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>r : AdicCompletion.AdicCauchySequence I R<GOAL>(Ideal.Quotient.mk (I ^ m)) (↑r n) = (Ideal.Quotient.mk (I ^ m)) (↑r m)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>r : AdicCompletion.AdicCauchySequence I R<VAR>x : AdicCompletion.AdicCauchySequence I M<GOAL>↑r n • Submodule.Quotient.mk (↑x n) = ↑r m • Submodule.Quotient.mk (↑x m)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>x : M<GOAL>(Ideal.Quotient.mk (I • ⊤)) r • Submodule.Quotient.mk x = r • Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>r : AdicCompletion I R<VAR>x : M ⧸ I ^ n • ⊤<GOAL>↑r n • x = (AdicCompletion.evalₐ I n) r • x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>r : AdicCompletion I R<VAR>x : AdicCompletion I M<GOAL>↑(r • x) n = ↑r n • ↑x n
<VAR>n : ℕ<GOAL>Polynomial.hermite (n + 1) = Polynomial.X * Polynomial.hermite n - Polynomial.derivative (Polynomial.hermite n)
<VAR>n : ℕ<GOAL>Polynomial.hermite n = (fun p => Polynomial.X * p - Polynomial.derivative p)^[n] 1
<VAR>n : ℕ<GOAL>(Polynomial.hermite (n + 1)).coeff 0 = -(Polynomial.hermite n).coeff 1
<VAR>n k : ℕ<GOAL>(Polynomial.hermite (n + 1)).coeff (k + 1) = (Polynomial.hermite n).coeff k - (↑k + 2) * (Polynomial.hermite n).coeff (k + 2)
<VAR>n k : ℕ<VAR>hnk : n < k<GOAL>(Polynomial.hermite n).coeff k = 0
<VAR>n : ℕ<GOAL>(Polynomial.hermite n).coeff n = 1
<VAR>n : ℕ<GOAL>(Polynomial.hermite n).degree = ↑n
<VAR>n : ℕ<GOAL>(Polynomial.hermite n).natDegree = n
<VAR>n : ℕ<GOAL>(Polynomial.hermite n).leadingCoeff = 1
<VAR>n : ℕ<GOAL>(Polynomial.hermite n).Monic
<VAR>n k : ℕ<VAR>hnk : Odd (n + k)<GOAL>(Polynomial.hermite n).coeff k = 0
<VAR>n k : ℕ<GOAL>(Polynomial.hermite (2 * n + k)).coeff k = (-1) ^ n * ↑(2 * n - 1).doubleFactorial * ↑((2 * n + k).choose k)
<VAR>n k : ℕ<VAR>hnk : Even (n + k)<GOAL>(Polynomial.hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1).doubleFactorial * ↑(n.choose k)
<VAR>n k : ℕ<GOAL>(Polynomial.hermite n).coeff k = if Even (n + k) then (-1) ^ ((n - k) / 2) * ↑(n - k - 1).doubleFactorial * ↑(n.choose k) else 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>p : R[X]<GOAL>(Polynomial.quotientSpanXSubCAlgEquiv x) ((Ideal.Quotient.mk (Ideal.span {Polynomial.X - Polynomial.C x})) p) = Polynomial.eval x p
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<GOAL>(Polynomial.quotientSpanXSubCAlgEquiv x).symm y = (algebraMap R (R[X] ⧸ Ideal.span {Polynomial.X - Polynomial.C x})) y
<VAR>R : Type u_1<VAR>CommRing R<VAR>p q : R[X]<VAR>hq : q.Monic<GOAL>p %ₘ q = 0 ↔ (Ideal.Quotient.mk (Ideal.span {q})) p = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>a : R<GOAL>a ∈ I → ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)).comp Polynomial.C) a = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>f : R[X]<GOAL>f ∈ Ideal.map Polynomial.C I → (Polynomial.eval₂RingHom (Polynomial.C.comp (Ideal.Quotient.mk I)) Polynomial.X) f = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>f : R[X]<GOAL>I.polynomialQuotientEquivQuotientPolynomial.symm ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f) = Polynomial.map (Ideal.Quotient.mk I) f
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>f : R[X]<GOAL>I.polynomialQuotientEquivQuotientPolynomial (Polynomial.map (Ideal.Quotient.mk I) f) = (Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Ideal R<GOAL>P.IsPrime → IsDomain (R[X] ⧸ Ideal.map Polynomial.C P)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R[X]<VAR>x : ↥((Ideal.Quotient.mk I).comp Polynomial.C).range<VAR>hx : Polynomial.C x ∈ Ideal.map (Polynomial.mapRingHom ((Ideal.Quotient.mk I).comp Polynomial.C).rangeRestrict) I<GOAL>x = 0
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>CommRing R<VAR>I : Ideal R<VAR>i : R<VAR>hi : i ∈ I<GOAL>((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) i = 0
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>CommRing R<VAR>I : Ideal R<VAR>a : MvPolynomial σ R<VAR>ha : a ∈ Ideal.map MvPolynomial.C I<GOAL>(MvPolynomial.eval₂Hom (MvPolynomial.C.comp (Ideal.Quotient.mk I)) MvPolynomial.X) a = 0
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>CommRing R<VAR>I : Ideal R<GOAL>Function.RightInverse (MvPolynomial.eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) ⋯) fun i => (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) (MvPolynomial.X i)) ⇑(Ideal.Quotient.lift (Ideal.map MvPolynomial.C I) (MvPolynomial.eval₂Hom (MvPolynomial.C.comp (Ideal.Quotient.mk I)) MvPolynomial.X) ⋯)
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>CommRing R<VAR>I : Ideal R<GOAL>Function.LeftInverse (MvPolynomial.eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) ⋯) fun i => (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) (MvPolynomial.X i)) ⇑(Ideal.Quotient.lift (Ideal.map MvPolynomial.C I) (MvPolynomial.eval₂Hom (MvPolynomial.C.comp (Ideal.Quotient.mk I)) MvPolynomial.X) ⋯)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g.Monic<VAR>hd : g ∣ Polynomial.map (algebraMap R K) f<GOAL>g ∈ Polynomial.lifts (algebraMap (↥(integralClosure R K)) K)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsIntegrallyClosed R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g ∣ Polynomial.map (algebraMap R K) f<GOAL>∃ g', Polynomial.map (algebraMap R K) g' * Polynomial.C g.leadingCoeff = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<GOAL>IsUnit f ↔ IsUnit (Polynomial.map φ f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<VAR>h_irr : Irreducible (Polynomial.map φ f)<GOAL>Irreducible f
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>p : R[X]<VAR>hp : p.IsPrimitive<GOAL>IsUnit p ↔ IsUnit (Polynomial.map (algebraMap R K) p)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsIntegrallyClosed R<VAR>p : R[X]<VAR>h : p.Monic<GOAL>Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<GOAL>IsIntegrallyClosed R ↔ ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p))
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsIntegrallyClosed R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>h : Polynomial.map (algebraMap R K) q ∣ Polynomial.map (algebraMap R K) p<GOAL>q ∣ p
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsIntegrallyClosed R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<GOAL>Polynomial.map (algebraMap R K) q ∣ Polynomial.map (algebraMap R K) p ↔ q ∣ p
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : K[X]<VAR>h0 : p ≠ 0<VAR>h : IsUnit (IsLocalization.integerNormalization R⁰ p).primPart<GOAL>IsUnit p
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<GOAL>Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<VAR>h_dvd : Polynomial.map (algebraMap R K) p ∣ Polynomial.map (algebraMap R K) q<GOAL>p ∣ q
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<GOAL>p ∣ q ↔ Polynomial.map (algebraMap R K) p ∣ Polynomial.map (algebraMap R K) q
<VAR>p : ℤ[X]<VAR>hp : p.IsPrimitive<GOAL>Irreducible p ↔ Irreducible (Polynomial.map (Int.castRingHom ℚ) p)
<VAR>p q : ℤ[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<GOAL>p ∣ q ↔ Polynomial.map (Int.castRingHom ℚ) p ∣ Polynomial.map (Int.castRingHom ℚ) q
<VAR>R : Type u_2<VAR>Semiring R<VAR>self : RingInvo R<VAR>x : R<GOAL>MulOpposite.unop (self.toFun (MulOpposite.unop (self.toFun x))) = x
<VAR>F : Type u_3<VAR>R : Type u_4<VAR>Semiring R<VAR>EquivLike F R Rᵐᵒᵖ<VAR>self : RingInvoClass F R<VAR>f : F<VAR>x : R<GOAL>MulOpposite.unop (f (MulOpposite.unop (f x))) = x
<VAR>R : Type u_2<VAR>Semiring R<VAR>f : RingInvo R<VAR>x : R<GOAL>MulOpposite.unop (f (MulOpposite.unop (f x))) = x
<VAR>R : Type u_2<VAR>Semiring R<VAR>f : RingInvo R<VAR>a : R<GOAL>↑f a = f a
<VAR>R : Type u_2<VAR>Semiring R<VAR>f : RingInvo R<VAR>x : R<GOAL>f x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>r : R<VAR>Semiring R<VAR>n : ℕ<VAR>hnil : IsNilpotent r<GOAL>IsNilpotent (Polynomial.C r * Polynomial.X ^ n)
<VAR>R : Type u_1<VAR>r : R<VAR>Semiring R<VAR>n : ℕ<VAR>hnil : IsNilpotent r<GOAL>IsNilpotent (Polynomial.X ^ n * Polynomial.C r)
<VAR>R : Type u_1<VAR>r : R<VAR>Semiring R<VAR>n : ℕ<GOAL>IsNilpotent ((Polynomial.monomial n) r) ↔ IsNilpotent r
<VAR>R : Type u_1<VAR>r : R<VAR>Semiring R<GOAL>IsNilpotent (Polynomial.C r) ↔ IsNilpotent r
<VAR>R : Type u_1<VAR>Semiring R<VAR>P : Polynomial R<GOAL>IsNilpotent (Polynomial.X * P) ↔ IsNilpotent P
<VAR>R : Type u_1<VAR>Semiring R<VAR>P : Polynomial R<GOAL>IsNilpotent (P * Polynomial.X) ↔ IsNilpotent P
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Polynomial R<GOAL>IsNilpotent P ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Polynomial R<VAR>N : ℕ<VAR>hN : P.natDegree ≤ N<GOAL>IsNilpotent (Polynomial.reflect N P) ↔ IsNilpotent P
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Polynomial R<GOAL>IsNilpotent P.reverse ↔ IsNilpotent P
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Polynomial R<VAR>hunit : IsUnit (P.coeff 0)<VAR>hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)<GOAL>IsUnit P
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Polynomial R<VAR>hunit : IsUnit P<GOAL>IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Polynomial R<GOAL>IsUnit P ↔ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
<VAR>R : Type u_1<VAR>r : R<VAR>CommRing R<VAR>P : Polynomial R<GOAL>IsUnit (Polynomial.C r + Polynomial.X * P) ↔ IsUnit r ∧ IsNilpotent P
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Polynomial R<GOAL>IsUnit P ↔ IsUnit (Polynomial.eval 0 P) ∧ IsNilpotent (P /ₘ Polynomial.X)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsReduced R<VAR>p : Polynomial R<VAR>hpl : 0 < p.natDegree<GOAL>¬IsUnit p
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsReduced R<VAR>p : Polynomial R<VAR>hpl : 0 < p.degree<GOAL>¬IsUnit p
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Polynomial R<VAR>a b : S<VAR>h : IsNilpotent (a - b)<GOAL>IsNilpotent ((Polynomial.aeval a) P - (Polynomial.aeval b) P)
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Polynomial R<VAR>a b : S<VAR>hb : IsUnit ((Polynomial.aeval b) P)<VAR>hab : IsNilpotent (a - b)<GOAL>IsUnit ((Polynomial.aeval a) P)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>ζ : R<VAR>i : ℕ<VAR>hi : i ∈ n.divisors<VAR>h : (Polynomial.cyclotomic i R).IsRoot ζ<GOAL>ζ ^ n = 1
<VAR>n : ℕ<VAR>h : 0 < n<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<GOAL>ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, (Polynomial.cyclotomic i R).IsRoot ζ
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>IsDomain R<VAR>hpos : 0 < n<VAR>μ : R<VAR>h : IsPrimitiveRoot μ n<GOAL>(Polynomial.cyclotomic n R).IsRoot μ
<VAR>n : ℕ<VAR>K : Type u_2<VAR>Field K<VAR>μ : K<VAR>NeZero ↑n<GOAL>(Polynomial.cyclotomic n K).IsRoot μ ↔ IsPrimitiveRoot μ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>IsDomain R<VAR>NeZero ↑n<VAR>μ : R<GOAL>(Polynomial.cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>IsDomain R<VAR>NeZero ↑n<GOAL>(Polynomial.cyclotomic n R).roots.Nodup
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>IsDomain R<VAR>NeZero ↑n<GOAL>{ val := (Polynomial.cyclotomic n R).roots, nodup := ⋯ } = primitiveRoots n R
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>IsDomain R<VAR>NeZero ↑n<GOAL>(Polynomial.cyclotomic n R).roots = (primitiveRoots n R).val
<VAR>n : ℕ<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>CharZero R<VAR>μ : R<VAR>hn : 0 < n<GOAL>(Polynomial.cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>CharZero R<GOAL>Function.Injective fun n => Polynomial.cyclotomic n R
<VAR>n : ℕ<VAR>K : Type u_2<VAR>Field K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>hpos : 0 < n<VAR>CharZero K<GOAL>minpoly ℤ μ ∣ Polynomial.cyclotomic n ℤ
<VAR>K : Type u_2<VAR>Field K<VAR>R : Type u_3<VAR>CommRing R<VAR>IsDomain R<VAR>μ : R<VAR>n : ℕ<VAR>Algebra K R<VAR>hμ : IsPrimitiveRoot μ n<VAR>h : Irreducible (Polynomial.cyclotomic n K)<VAR>NeZero ↑n<GOAL>Polynomial.cyclotomic n K = minpoly K μ
<VAR>n : ℕ<VAR>K : Type u_2<VAR>Field K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>hpos : 0 < n<VAR>CharZero K<GOAL>Polynomial.cyclotomic n ℤ = minpoly ℤ μ
<VAR>n : ℕ<VAR>K : Type u_2<VAR>Field K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>hpos : 0 < n<VAR>CharZero K<GOAL>Polynomial.cyclotomic n ℚ = minpoly ℚ μ
<VAR>n : ℕ<VAR>hpos : 0 < n<GOAL>Irreducible (Polynomial.cyclotomic n ℤ)
<VAR>n : ℕ<VAR>hpos : 0 < n<GOAL>Irreducible (Polynomial.cyclotomic n ℚ)
<VAR>n m : ℕ<VAR>h : n ≠ m<GOAL>IsCoprime (Polynomial.cyclotomic n ℚ) (Polynomial.cyclotomic m ℚ)
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<VAR>𝓟 : Ideal R<GOAL>f.IsWeaklyEisensteinAt 𝓟 ↔ ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<VAR>𝓟 : Ideal R<VAR>self : f.IsWeaklyEisensteinAt 𝓟<VAR>n : ℕ<GOAL>n < f.natDegree → f.coeff n ∈ 𝓟
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<VAR>𝓟 : Ideal R<VAR>self : f.IsEisensteinAt 𝓟<VAR>n : ℕ<GOAL>n < f.natDegree → f.coeff n ∈ 𝓟
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<VAR>𝓟 : Ideal R<GOAL>f.IsEisensteinAt 𝓟 ↔ f.leadingCoeff ∉ 𝓟 ∧ (∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟) ∧ f.coeff 0 ∉ 𝓟 ^ 2
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<VAR>𝓟 : Ideal R<VAR>self : f.IsEisensteinAt 𝓟<GOAL>f.leadingCoeff ∉ 𝓟
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<VAR>𝓟 : Ideal R<VAR>self : f.IsEisensteinAt 𝓟<GOAL>f.coeff 0 ∉ 𝓟 ^ 2
<VAR>R : Type u<VAR>CommSemiring R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(Polynomial.map φ f).IsWeaklyEisensteinAt (Ideal.map φ 𝓟)
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>p : R<VAR>x : S<VAR>hx : (Polynomial.aeval x) f = 0<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<GOAL>∃ y ∈ Algebra.adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>p : R<VAR>x : S<VAR>hx : (Polynomial.aeval x) f = 0<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<VAR>i : ℕ<GOAL>(Polynomial.map (algebraMap R S) f).natDegree ≤ i → ∃ y ∈ Algebra.adjoin R {x}, (algebraMap R S) p * y = x ^ i
<VAR>R : Type u<VAR>CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>x : R<VAR>hroot : f.IsRoot x<VAR>hmo : f.Monic<VAR>i : ℕ<GOAL>f.natDegree ≤ i → x ^ i ∈ 𝓟
<VAR>R : Type u<VAR>CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>hx : (Polynomial.aeval x) f = 0<VAR>hmo : f.Monic<VAR>i : ℕ<GOAL>(Polynomial.map (algebraMap R S) f).natDegree ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>x : R<VAR>P : Ideal R<VAR>hP : x ∈ P<GOAL>(p.scaleRoots x).IsWeaklyEisensteinAt P
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommRing R<VAR>CommRing A<VAR>f : R →+* A<VAR>hf : Function.Injective ⇑f<VAR>p : R[X]<VAR>hp : p.Monic<VAR>x y : R<VAR>z : A<VAR>h : Polynomial.eval₂ f z p = 0<VAR>hz : f x * z = f y<GOAL>x ∣ y ^ p.natDegree
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>Nontrivial A<VAR>NoZeroSMulDivisors R A<VAR>p : R[X]<VAR>hp : p.Monic<VAR>x y : R<VAR>z : A<VAR>h : (Polynomial.aeval z) p = 0<VAR>hz : z * (algebraMap R A) x = (algebraMap R A) y<GOAL>x ∣ y ^ p.natDegree
<VAR>R : Type u<VAR>CommSemiring R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>h : 𝓟 ≠ ⊤<GOAL>f.leadingCoeff ∉ 𝓟
<VAR>R : Type u<VAR>CommSemiring R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>h : 𝓟 ≠ ⊤<VAR>hmem : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟<VAR>hnot_mem : f.coeff 0 ∉ 𝓟 ^ 2<GOAL>f.IsEisensteinAt 𝓟
<VAR>R : Type u<VAR>CommSemiring R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsEisensteinAt 𝓟<GOAL>f.IsWeaklyEisensteinAt 𝓟
<VAR>R : Type u<VAR>CommSemiring R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsEisensteinAt 𝓟<VAR>n : ℕ<VAR>hn : n ≠ f.natDegree<GOAL>f.coeff n ∈ 𝓟
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsEisensteinAt 𝓟<VAR>hprime : 𝓟.IsPrime<VAR>hu : f.IsPrimitive<VAR>hfd0 : 0 < f.natDegree<GOAL>Irreducible f
<GOAL>RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral
<GOAL>RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral
<GOAL>RingHom.StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : ¬p ∣ n<VAR>R : Type u_1<VAR>CommRing R<GOAL>(Polynomial.expand R p) (Polynomial.cyclotomic n R) = Polynomial.cyclotomic (n * p) R * Polynomial.cyclotomic n R
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : p ∣ n<VAR>R : Type u_1<VAR>CommRing R<GOAL>(Polynomial.expand R p) (Polynomial.cyclotomic n R) = Polynomial.cyclotomic (n * p) R
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>n m : ℕ<VAR>hmn : m ≤ n<VAR>h : Irreducible (Polynomial.cyclotomic (p ^ n) R)<GOAL>Irreducible (Polynomial.cyclotomic (p ^ m) R)
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : Irreducible (Polynomial.cyclotomic (p ^ n) R)<GOAL>Irreducible (Polynomial.cyclotomic p R)
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>Ring R<VAR>CharP R p<VAR>hn : ¬p ∣ n<GOAL>Polynomial.cyclotomic (n * p) R = Polynomial.cyclotomic n R ^ (p - 1)
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>Ring R<VAR>CharP R p<VAR>hn : p ∣ n<GOAL>Polynomial.cyclotomic (n * p) R = Polynomial.cyclotomic n R ^ p
<VAR>R : Type u_1<VAR>p m : ℕ<VAR>Fact (Nat.Prime p)<VAR>Ring R<VAR>CharP R p<VAR>hm : ¬p ∣ m<VAR>k : ℕ<GOAL>0 < k → Polynomial.cyclotomic (p ^ k * m) R = Polynomial.cyclotomic m R ^ (p ^ k - p ^ (k - 1))
<VAR>m k p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>hp : Fact (Nat.Prime p)<VAR>hchar : CharP R p<VAR>μ : R<VAR>NeZero ↑m<GOAL>(Polynomial.cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m
<GOAL>RingHom.StableUnderComposition @RingHom.Finite
<GOAL>RingHom.RespectsIso @RingHom.Finite
<GOAL>RingHom.StableUnderBaseChange @RingHom.Finite
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>self : IsHausdorff I M<VAR>x : M<GOAL>(∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]) → x = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>self : IsPrecomplete I M<VAR>f : ℕ → M<GOAL>(∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]) → ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<GOAL>IsHausdorff I M → ∀ (x : M), (∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]) → x = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<GOAL>IsHausdorff I M ↔ ∀ (x : M), (∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]) → x = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<GOAL>IsPrecomplete I M → ∀ {f : ℕ → M}, (∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]) → ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<GOAL>IsPrecomplete I M ↔ ∀ (f : ℕ → M), (∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]) → ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>h : IsHausdorff ⊤ M<GOAL>Subsingleton M
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>h : IsHausdorff I M<GOAL>⨅ n, I ^ n • ⊤ = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>C : Hausdorffification I M → Prop<VAR>x : Hausdorffification I M<VAR>ih : ∀ (x : M), C ((Hausdorffification.of I M) x)<GOAL>C x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>h : IsHausdorff I N<VAR>f : M →ₗ[R] N<VAR>x : M<GOAL>(Hausdorffification.lift I f) ((Hausdorffification.of I M) x) = f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>h : IsHausdorff I N<VAR>f : M →ₗ[R] N<GOAL>Hausdorffification.lift I f ∘ₗ Hausdorffification.of I M = f
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>h : IsHausdorff I N<VAR>f : M →ₗ[R] N<VAR>g : Hausdorffification I M →ₗ[R] N<VAR>hg : g ∘ₗ Hausdorffification.of I M = f<GOAL>g = Hausdorffification.lift I f
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x : AdicCompletion I M<VAR>n : ℕ<GOAL>(AdicCompletion.incl I M) x n = ↑x n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>n : ℕ<GOAL>↑((AdicCompletion.of I M) x) n = (I ^ n • ⊤).mkQ x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<GOAL>⇑(AdicCompletion.eval I M n) = fun f => ↑f n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>f : AdicCompletion I M<GOAL>(AdicCompletion.eval I M n) f = ↑f n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>x : M<GOAL>(AdicCompletion.eval I M n) ((AdicCompletion.of I M) x) = (I ^ n • ⊤).mkQ x