ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : MeasureTheory.Integrable (X 0) ℙ<VAR>h' : MeasureTheory.StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<GOAL>∀ᵐ (ω : Ω), Filter.Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) Filter.atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : MeasureTheory.Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<GOAL>∀ᵐ (ω : Ω), Filter.Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) Filter.atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>X : ℕ → Ω → E<VAR>hℒp : MeasureTheory.Memℒp (X 0) p ℙ<VAR>hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (fun ω => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω - ∫ (a : Ω), X 0 a) p ℙ) Filter.atTop (𝓝 0)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ : MvPowerSeries σ R<VAR>hφ : (MvPowerSeries.constantCoeff σ R) φ ∈ nonZeroDivisors R<GOAL>φ ∈ nonZeroDivisors (MvPowerSeries σ R)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>x : WittVector p R<VAR>n k : ℕ<GOAL>(x.shift n).coeff k = x.coeff (n + k)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<VAR>k : ℕ<VAR>h : ∀ i < k + 1, x.coeff i = 0<GOAL>WittVector.verschiebung (x.shift k.succ) = x.shift k
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<VAR>n : ℕ<VAR>h : ∀ i < n, x.coeff i = 0<GOAL>x = (⇑WittVector.verschiebung)^[n] (x.shift n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<VAR>hx : x ≠ 0<GOAL>∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑WittVector.verschiebung)^[n] x'
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>n : ℕ<VAR>x : WittVector p R<VAR>k : ℕ<GOAL>(x * ↑n).coeff k = (MvPolynomial.aeval x.coeff) (WittVector.wittMulN p n k)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>WittVector.IsPoly p fun R _Rcr x => x * ↑n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n k : ℕ<GOAL>(MvPolynomial.bind₁ (WittVector.wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<GOAL>Polynomial.cyclotomic' 0 R = 1
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<GOAL>Polynomial.cyclotomic' 1 R = Polynomial.X - 1
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>CharP R p<VAR>hp : p ≠ 2<GOAL>Polynomial.cyclotomic' 2 R = Polynomial.X + 1
<VAR>n : ℕ<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<GOAL>(Polynomial.cyclotomic' n R).Monic
<VAR>n : ℕ<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<GOAL>Polynomial.cyclotomic' n R ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>(Polynomial.cyclotomic' n R).natDegree = n.totient
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>(Polynomial.cyclotomic' n R).degree = ↑n.totient
<VAR>n : ℕ<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<GOAL>(Polynomial.cyclotomic' n R).roots = (primitiveRoots n R).val
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<GOAL>Polynomial.X ^ n - 1 = ∏ ζ ∈ Polynomial.nthRootsFinset n R, (Polynomial.X - Polynomial.C ζ)
<VAR>K : Type u_1<VAR>Field K<VAR>n : ℕ<GOAL>Polynomial.Splits (RingHom.id K) (Polynomial.cyclotomic' n K)
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>Polynomial.Splits (RingHom.id K) (Polynomial.X ^ n - Polynomial.C 1)
<VAR>K : Type u_2<VAR>CommRing K<VAR>IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<GOAL>∏ i ∈ n.divisors, Polynomial.cyclotomic' i K = Polynomial.X ^ n - 1
<VAR>K : Type u_2<VAR>CommRing K<VAR>IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<GOAL>Polynomial.cyclotomic' n K = (Polynomial.X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, Polynomial.cyclotomic' i K
<VAR>K : Type u_2<VAR>CommRing K<VAR>IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>∃ P, Polynomial.map (Int.castRingHom K) P = Polynomial.cyclotomic' n K ∧ P.degree = (Polynomial.cyclotomic' n K).degree ∧ P.Monic
<VAR>K : Type u_2<VAR>CommRing K<VAR>IsDomain K<VAR>CharZero K<VAR>ζ : K<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<GOAL>∃! P, Polynomial.map (Int.castRingHom K) P = Polynomial.cyclotomic' (↑n) K
<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Polynomial.cyclotomic n ℤ = ⋯.choose
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<GOAL>Polynomial.map (Int.castRingHom R) (Polynomial.cyclotomic n ℤ) = Polynomial.cyclotomic n R
<VAR>n : ℕ<GOAL>Polynomial.map (Int.castRingHom ℂ) (Polynomial.cyclotomic n ℤ) = Polynomial.cyclotomic' n ℂ ∧ (Polynomial.cyclotomic n ℤ).degree = (Polynomial.cyclotomic' n ℂ).degree ∧ (Polynomial.cyclotomic n ℤ).Monic
<VAR>n : ℕ<VAR>P : ℤ[X]<VAR>h : Polynomial.map (Int.castRingHom ℂ) P = Polynomial.cyclotomic' n ℂ<GOAL>P = Polynomial.cyclotomic n ℤ
<VAR>n : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>Polynomial.map f (Polynomial.cyclotomic n R) = Polynomial.cyclotomic n S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>q : R<VAR>n : ℕ<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>Polynomial.eval (f q) (Polynomial.cyclotomic n S) = f (Polynomial.eval q (Polynomial.cyclotomic n R))
<VAR>R : Type u_1<VAR>Ring R<GOAL>Polynomial.cyclotomic 0 R = 1
<VAR>R : Type u_1<VAR>Ring R<GOAL>Polynomial.cyclotomic 1 R = Polynomial.X - 1
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<GOAL>(Polynomial.cyclotomic n R).Monic
<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<GOAL>(Polynomial.cyclotomic n R).IsPrimitive
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>Nontrivial R<GOAL>Polynomial.cyclotomic n R ≠ 0
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>Nontrivial R<GOAL>(Polynomial.cyclotomic n R).degree = ↑n.totient
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>Nontrivial R<GOAL>(Polynomial.cyclotomic n R).natDegree = n.totient
<VAR>n : ℕ<VAR>R : Type u_1<VAR>hpos : 0 < n<VAR>Ring R<VAR>Nontrivial R<GOAL>0 < (Polynomial.cyclotomic n R).degree
<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>R : Type u_1<VAR>CommRing R<GOAL>∏ i ∈ n.divisors, Polynomial.cyclotomic i R = Polynomial.X ^ n - 1
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<GOAL>Polynomial.cyclotomic n R ∣ Polynomial.X ^ n - 1
<VAR>n : ℕ<VAR>h : 0 < n<VAR>R : Type u_1<VAR>CommRing R<GOAL>∏ i ∈ n.divisors.erase 1, Polynomial.cyclotomic i R = ∑ i ∈ Finset.range n, Polynomial.X ^ i
<VAR>R : Type u_1<VAR>Ring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>Polynomial.cyclotomic p R = ∑ i ∈ Finset.range p, Polynomial.X ^ i
<VAR>R : Type u_1<VAR>Ring R<VAR>p : ℕ<VAR>hn : Fact (Nat.Prime p)<GOAL>Polynomial.cyclotomic p R * (Polynomial.X - 1) = Polynomial.X ^ p - 1
<VAR>R : Type u_1<VAR>Ring R<GOAL>Polynomial.cyclotomic 2 R = Polynomial.X + 1
<VAR>R : Type u_1<VAR>Ring R<GOAL>Polynomial.cyclotomic 3 R = Polynomial.X ^ 2 + Polynomial.X + 1
<VAR>R : Type u_1<VAR>Ring R<VAR>d n : ℕ<VAR>hdn : d ∣ n<VAR>hd : d ≠ 1<GOAL>Polynomial.cyclotomic d R ∣ ∑ i ∈ Finset.range n, Polynomial.X ^ i
<VAR>R : Type u_1<VAR>CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<GOAL>(Polynomial.X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, Polynomial.cyclotomic x R = Polynomial.X ^ n - 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<GOAL>(Polynomial.X ^ d - 1) * Polynomial.cyclotomic n R ∣ Polynomial.X ^ n - 1
<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<GOAL>(algebraMap R[X] (RatFunc R)) (Polynomial.cyclotomic n R) = ∏ i ∈ n.divisorsAntidiagonal, (algebraMap R[X] (RatFunc R)) (Polynomial.X ^ i.2 - 1) ^ ArithmeticFunction.moebius i.1
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>hpos : 0 < n<GOAL>Polynomial.cyclotomic n R = (Polynomial.X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i R
<VAR>R : Type u_1<VAR>CommRing R<VAR>n m : ℕ<VAR>hpos : 0 < n<VAR>hm : m ∣ n<VAR>hdiff : m ≠ n<GOAL>Polynomial.X ^ m - 1 ∣ ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i R
<VAR>K : Type u_1<VAR>CommRing K<VAR>IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hz : IsPrimitiveRoot ζ n<GOAL>Polynomial.cyclotomic n K = ∏ μ ∈ primitiveRoots n K, (Polynomial.X - Polynomial.C μ)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>P : R[X]<GOAL>P = Polynomial.cyclotomic n R ↔ P * ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i R = Polynomial.X ^ n - 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>p n : ℕ<VAR>hp : Nat.Prime p<GOAL>Polynomial.cyclotomic (p ^ (n + 1)) R = ∑ i ∈ Finset.range p, (Polynomial.X ^ p ^ n) ^ i
<VAR>R : Type u_1<VAR>CommRing R<VAR>p k : ℕ<VAR>hn : Fact (Nat.Prime p)<GOAL>Polynomial.cyclotomic (p ^ (k + 1)) R * (Polynomial.X ^ p ^ k - 1) = Polynomial.X ^ p ^ (k + 1) - 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>hn : 1 < n<GOAL>(Polynomial.cyclotomic n R).coeff 0 = 1
<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>p : ℕ<VAR>hprime : Fact (Nat.Prime p)<VAR>a : ℕ<VAR>hroot : (Polynomial.cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)<GOAL>a.Coprime p
<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℕ<VAR>hroot : (Polynomial.cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)<GOAL>orderOf (ZMod.unitOfCoprime a ⋯) ∣ n
<VAR>motive : ℤ → Prop<VAR>zero : motive 0<VAR>one : motive 1<VAR>add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)<VAR>neg_add_one : ∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)<VAR>a : ℤ<GOAL>motive a
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.T R (n + 2) = 2 * Polynomial.X * Polynomial.Chebyshev.T R (n + 1) - Polynomial.Chebyshev.T R n
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.T R (n + 1) = 2 * Polynomial.X * Polynomial.Chebyshev.T R n - Polynomial.Chebyshev.T R (n - 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.T R (n - 2) = 2 * Polynomial.X * Polynomial.Chebyshev.T R (n - 1) - Polynomial.Chebyshev.T R n
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.T R (n - 1) = 2 * Polynomial.X * Polynomial.Chebyshev.T R n - Polynomial.Chebyshev.T R (n + 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.T R n = 2 * Polynomial.X * Polynomial.Chebyshev.T R (n - 1) - Polynomial.Chebyshev.T R (n - 2)
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Polynomial.Chebyshev.T R 0 = 1
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Polynomial.Chebyshev.T R 1 = Polynomial.X
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Polynomial.Chebyshev.T R (-1) = Polynomial.X
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Polynomial.Chebyshev.T R 2 = 2 * Polynomial.X ^ 2 - 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.T R (-n) = Polynomial.Chebyshev.T R n
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.T R ↑n.natAbs = Polynomial.Chebyshev.T R n
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Polynomial.Chebyshev.T R (-2) = 2 * Polynomial.X ^ 2 - 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.U R (n + 2) = 2 * Polynomial.X * Polynomial.Chebyshev.U R (n + 1) - Polynomial.Chebyshev.U R n
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.U R (n + 1) = 2 * Polynomial.X * Polynomial.Chebyshev.U R n - Polynomial.Chebyshev.U R (n - 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.U R (n - 2) = 2 * Polynomial.X * Polynomial.Chebyshev.U R (n - 1) - Polynomial.Chebyshev.U R n
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.U R (n - 1) = 2 * Polynomial.X * Polynomial.Chebyshev.U R n - Polynomial.Chebyshev.U R (n + 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.U R n = 2 * Polynomial.X * Polynomial.Chebyshev.U R (n - 1) - Polynomial.Chebyshev.U R (n - 2)
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Polynomial.Chebyshev.U R 0 = 1
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Polynomial.Chebyshev.U R 1 = 2 * Polynomial.X
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Polynomial.Chebyshev.U R (-1) = 0
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Polynomial.Chebyshev.U R 2 = 4 * Polynomial.X ^ 2 - 1
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Polynomial.Chebyshev.U R (-2) = -1
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.U R (-n - 1) = -Polynomial.Chebyshev.U R (n - 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.U R (-n) = -Polynomial.Chebyshev.U R (n - 2)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.U R (-n - 2) = -Polynomial.Chebyshev.U R n
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.U R (n + 1) = Polynomial.X * Polynomial.Chebyshev.U R n + Polynomial.Chebyshev.T R (n + 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.T R n = Polynomial.Chebyshev.U R n - Polynomial.X * Polynomial.Chebyshev.U R (n - 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.Chebyshev.T R (n + 2) = Polynomial.X * Polynomial.Chebyshev.T R (n + 1) - (1 - Polynomial.X ^ 2) * Polynomial.Chebyshev.U R n
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>(1 - Polynomial.X ^ 2) * Polynomial.Chebyshev.U R n = Polynomial.X * Polynomial.Chebyshev.T R (n + 1) - Polynomial.Chebyshev.T R (n + 2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>n : ℤ<GOAL>Polynomial.map f (Polynomial.Chebyshev.T R n) = Polynomial.Chebyshev.T S n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>n : ℤ<GOAL>Polynomial.map f (Polynomial.Chebyshev.U R n) = Polynomial.Chebyshev.U S n
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>Polynomial.derivative (Polynomial.Chebyshev.T R n) = ↑n * Polynomial.Chebyshev.U R (n - 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>(1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.Chebyshev.T R (n + 1)) = (↑n + 1) * (Polynomial.Chebyshev.T R n - Polynomial.X * Polynomial.Chebyshev.T R (n + 1))
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℤ<GOAL>(↑n + 1) * Polynomial.Chebyshev.T R (n + 1) = Polynomial.X * Polynomial.Chebyshev.U R n - (1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.Chebyshev.U R n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>m k : ℤ<GOAL>2 * Polynomial.Chebyshev.T R m * Polynomial.Chebyshev.T R k = Polynomial.Chebyshev.T R (m + k) + Polynomial.Chebyshev.T R (m - k)
<VAR>R : Type u_1<VAR>CommRing R<VAR>m n : ℤ<GOAL>Polynomial.Chebyshev.T R (m * n) = (Polynomial.Chebyshev.T R m).comp (Polynomial.Chebyshev.T R n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>hn : Fact (Nat.Prime p)<GOAL>Polynomial.eval 1 (Polynomial.cyclotomic p R) = ↑p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>Polynomial.eval₂ f 1 (Polynomial.cyclotomic p R) = ↑p
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>k : ℕ<VAR>hn : Fact (Nat.Prime p)<GOAL>Polynomial.eval 1 (Polynomial.cyclotomic (p ^ (k + 1)) R) = ↑p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Semiring S<VAR>f : R →+* S<VAR>p : ℕ<VAR>k : ℕ<VAR>Fact (Nat.Prime p)<GOAL>Polynomial.eval₂ f 1 (Polynomial.cyclotomic (p ^ (k + 1)) R) = ↑p
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<GOAL>0 < Polynomial.eval (-1) (Polynomial.cyclotomic n R)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>x : R<GOAL>0 < Polynomial.eval x (Polynomial.cyclotomic n R)
<VAR>n : ℕ<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>x : R<GOAL>(1 < x → 0 < Polynomial.eval x (Polynomial.cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ Polynomial.eval x (Polynomial.cyclotomic n R))
<VAR>n : ℕ<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>x : R<VAR>hx : 1 < x<GOAL>0 < Polynomial.eval x (Polynomial.cyclotomic n R)
<VAR>n : ℕ<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>x : R<VAR>hx : 1 ≤ x<GOAL>0 ≤ Polynomial.eval x (Polynomial.cyclotomic n R)
<VAR>R : Type u_1<VAR>Ring R<VAR>n : ℕ<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n<GOAL>Polynomial.eval 1 (Polynomial.cyclotomic n R) = 1
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<GOAL>(q - 1) ^ n.totient < Polynomial.eval q (Polynomial.cyclotomic n ℝ)
<VAR>q : ℝ<VAR>hq' : 1 < q<VAR>n : ℕ<GOAL>(q - 1) ^ n.totient ≤ Polynomial.eval q (Polynomial.cyclotomic n ℝ)
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<GOAL>Polynomial.eval q (Polynomial.cyclotomic n ℝ) < (q + 1) ^ n.totient
<VAR>q : ℝ<VAR>hq' : 1 < q<VAR>n : ℕ<GOAL>Polynomial.eval q (Polynomial.cyclotomic n ℝ) ≤ (q + 1) ^ n.totient
<VAR>n q : ℕ<VAR>hn' : 1 < n<VAR>hq : q ≠ 1<GOAL>(q - 1) ^ n.totient < (Polynomial.eval (↑q) (Polynomial.cyclotomic n ℤ)).natAbs
<VAR>n q : ℕ<VAR>hn' : 1 < n<VAR>hq : q ≠ 1<GOAL>q - 1 < (Polynomial.eval (↑q) (Polynomial.cyclotomic n ℤ)).natAbs
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>r : R<VAR>n : ℕ<GOAL>(WittVector.ghostComponent n) (WittVector.teichmullerFun p r) = r ^ p ^ n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>r : R<GOAL>(WittVector.map f) (WittVector.teichmullerFun p r) = WittVector.teichmullerFun p (f r)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>x y : MvPolynomial R ℚ<GOAL>WittVector.teichmullerFun p (x * y) = WittVector.teichmullerFun p x * WittVector.teichmullerFun p y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>x y : MvPolynomial R ℤ<GOAL>WittVector.teichmullerFun p (x * y) = WittVector.teichmullerFun p x * WittVector.teichmullerFun p y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>r : R<GOAL>((WittVector.teichmuller p) r).coeff 0 = r
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>r : R<VAR>n : ℕ<GOAL>0 < n → ((WittVector.teichmuller p) r).coeff n = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<GOAL>(WittVector.teichmuller p) 0 = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>r : R<GOAL>(WittVector.map f) ((WittVector.teichmuller p) r) = (WittVector.teichmuller p) (f r)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>r : R<VAR>n : ℕ<GOAL>(WittVector.ghostComponent n) ((WittVector.teichmuller p) r) = r ^ p ^ n
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Ring R<VAR>DecidableEq σ<VAR>n : σ →₀ ℕ<VAR>a : R<VAR>φ : MvPowerSeries σ R<GOAL>(MvPowerSeries.coeff R n) (MvPowerSeries.inv.aux a φ) = if n = 0 then a else -a * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (MvPowerSeries.coeff R x.1) φ * (MvPowerSeries.coeff R x.2) (MvPowerSeries.inv.aux a φ) else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Ring R<VAR>DecidableEq σ<VAR>n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<VAR>u : Rˣ<GOAL>(MvPowerSeries.coeff R n) (φ.invOfUnit u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (MvPowerSeries.coeff R x.1) φ * (MvPowerSeries.coeff R x.2) (φ.invOfUnit u) else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Ring R<VAR>φ : MvPowerSeries σ R<VAR>u : Rˣ<GOAL>(MvPowerSeries.constantCoeff σ R) (φ.invOfUnit u) = ↑u⁻¹
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Ring R<VAR>φ : MvPowerSeries σ R<VAR>u : Rˣ<VAR>h : (MvPowerSeries.constantCoeff σ R) φ = ↑u<GOAL>φ * φ.invOfUnit u = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Ring R<VAR>φ : MvPowerSeries σ R<VAR>u : Rˣ<VAR>h : (MvPowerSeries.constantCoeff σ R) φ = ↑u<GOAL>φ.invOfUnit u * φ = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Ring R<VAR>φ : MvPowerSeries σ R<GOAL>IsUnit φ ↔ IsUnit ((MvPowerSeries.constantCoeff σ R) φ)
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>DecidableEq σ<VAR>n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ k<GOAL>(MvPowerSeries.coeff k n) φ⁻¹ = if n = 0 then ((MvPowerSeries.constantCoeff σ k) φ)⁻¹ else -((MvPowerSeries.constantCoeff σ k) φ)⁻¹ * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (MvPowerSeries.coeff k x.1) φ * (MvPowerSeries.coeff k x.2) φ⁻¹ else 0
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>φ : MvPowerSeries σ k<GOAL>(MvPowerSeries.constantCoeff σ k) φ⁻¹ = ((MvPowerSeries.constantCoeff σ k) φ)⁻¹
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>φ : MvPowerSeries σ k<GOAL>φ⁻¹ = 0 ↔ (MvPowerSeries.constantCoeff σ k) φ = 0
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<GOAL>0⁻¹ = 0
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>φ : MvPowerSeries σ k<VAR>h : (MvPowerSeries.constantCoeff σ k) φ ≠ 0<GOAL>φ.invOfUnit (Units.mk0 ((MvPowerSeries.constantCoeff σ k) φ) h) = φ⁻¹
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>φ : MvPowerSeries σ k<VAR>u : kˣ<VAR>h : (MvPowerSeries.constantCoeff σ k) φ = ↑u<GOAL>φ.invOfUnit u = φ⁻¹
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>φ : MvPowerSeries σ k<VAR>h : (MvPowerSeries.constantCoeff σ k) φ ≠ 0<GOAL>φ * φ⁻¹ = 1
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>φ : MvPowerSeries σ k<VAR>h : (MvPowerSeries.constantCoeff σ k) φ ≠ 0<GOAL>φ⁻¹ * φ = 1
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>φ₁ φ₂ φ₃ : MvPowerSeries σ k<VAR>h : (MvPowerSeries.constantCoeff σ k) φ₃ ≠ 0<GOAL>φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>φ ψ : MvPowerSeries σ k<VAR>h : (MvPowerSeries.constantCoeff σ k) ψ ≠ 0<GOAL>φ = ψ⁻¹ ↔ φ * ψ = 1
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>φ ψ : MvPowerSeries σ k<VAR>h : (MvPowerSeries.constantCoeff σ k) ψ ≠ 0<GOAL>ψ⁻¹ = φ ↔ φ * ψ = 1
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>φ ψ : MvPowerSeries σ k<GOAL>(φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>r : k<GOAL>((MvPowerSeries.C σ k) r)⁻¹ = (MvPowerSeries.C σ k) r⁻¹
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>s : σ<GOAL>(MvPowerSeries.X s)⁻¹ = 0
<VAR>σ : Type u_1<VAR>k : Type u_3<VAR>Field k<VAR>r : k<VAR>φ : MvPowerSeries σ k<GOAL>(r • φ)⁻¹ = r⁻¹ • φ⁻¹
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<GOAL>WittVector.frobenius (WittVector.verschiebung x) = x * ↑p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : WittVector p (ZMod p)<GOAL>WittVector.verschiebung x = x * ↑p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>i : ℕ<GOAL>(↑p ^ i).coeff i = 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>i j : ℕ<VAR>hj : j ≠ i<GOAL>(↑p ^ i).coeff j = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>i : ℕ<GOAL>(↑p).coeff i = if i = 1 then 1 else 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<GOAL>(↑p).coeff 0 = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<GOAL>(↑p).coeff 1 = 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>Nontrivial R<VAR>CharP R p<GOAL>↑p ≠ 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x y : WittVector p R<GOAL>WittVector.verschiebung (x * WittVector.frobenius y) = WittVector.verschiebung x * y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>x : WittVector p R<GOAL>(x * ↑p).coeff 0 = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>x : WittVector p R<VAR>i : ℕ<GOAL>(x * ↑p).coeff (i + 1) = x.coeff i ^ p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>x : WittVector p R<GOAL>WittVector.verschiebung (WittVector.frobenius x) = x * ↑p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<GOAL>Function.Commute ⇑WittVector.verschiebung ⇑WittVector.frobenius
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<VAR>n k : ℕ<GOAL>((⇑WittVector.verschiebung)^[n] x).coeff (k + n) = x.coeff k