ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(WittVector.wittSub p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(WittVector.wittMul p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(WittVector.wittNeg p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m n : ℕ<GOAL>(WittVector.wittNSMul p m n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m : ℤ<VAR>n : ℕ<GOAL>(WittVector.wittZSMul p m n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m n : ℕ<GOAL>(WittVector.wittPow p m n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<GOAL>W_ R n = ∑ i ∈ Finset.range (n + 1), MvPolynomial.C (↑p ^ i) * MvPolynomial.X i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>(MvPolynomial.map f) (W_ R n) = W_ S n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>MvPolynomial.constantCoeff (W_ R n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<GOAL>W_ R 0 = MvPolynomial.X 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<GOAL>W_ R 1 = MvPolynomial.C ↑p * MvPolynomial.X 1 + MvPolynomial.X 0 ^ p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_3<VAR>CommRing A<VAR>Algebra R A<VAR>f : ℕ → A<VAR>n : ℕ<GOAL>(MvPolynomial.aeval f) (W_ R n) = ∑ i ∈ Finset.range (n + 1), ↑p ^ i * f i ^ p ^ (n - i)
<VAR>p n : ℕ<GOAL>W_ (ZMod (p ^ (n + 1))) (n + 1) = (MvPolynomial.expand p) (W_ (ZMod (p ^ (n + 1))) n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>hp : NeZero p<VAR>CharZero R<VAR>n : ℕ<GOAL>(W_ R n).vars = Finset.range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>hp : NeZero p<VAR>n : ℕ<GOAL>(W_ R n).vars ⊆ Finset.range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>Invertible ↑p<VAR>n : ℕ<GOAL>xInTermsOfW p R n = (MvPolynomial.X n - ∑ i ∈ Finset.range n, MvPolynomial.C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * MvPolynomial.C (⅟↑p ^ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Invertible ↑p<VAR>n : ℕ<GOAL>MvPolynomial.constantCoeff (xInTermsOfW p R n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>Invertible ↑p<GOAL>xInTermsOfW p R 0 = MvPolynomial.X 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>n ∈ (xInTermsOfW p ℚ n).vars ∧ (xInTermsOfW p ℚ n).vars ⊆ Finset.range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(xInTermsOfW p ℚ n).vars ⊆ Finset.range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>Invertible ↑p<VAR>n : ℕ<GOAL>xInTermsOfW p R n * MvPolynomial.C (↑p ^ n) = MvPolynomial.X n - ∑ i ∈ Finset.range n, MvPolynomial.C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>Invertible ↑p<VAR>k : ℕ<GOAL>(MvPolynomial.bind₁ (xInTermsOfW p R)) (W_ R k) = MvPolynomial.X k
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>Invertible ↑p<VAR>n : ℕ<GOAL>(MvPolynomial.bind₁ (W_ R)) (xInTermsOfW p R n) = MvPolynomial.X n
<VAR>R : Type u<VAR>Semiring R<VAR>n : WithBot ℕ<VAR>f : R[X]<GOAL>f ∈ Polynomial.degreeLE R n ↔ f.degree ≤ n
<VAR>R : Type u<VAR>Semiring R<VAR>m n : WithBot ℕ<VAR>H : m ≤ n<GOAL>Polynomial.degreeLE R m ≤ Polynomial.degreeLE R n
<VAR>R : Type u<VAR>Semiring R<VAR>DecidableEq R<VAR>n : ℕ<GOAL>Polynomial.degreeLE R ↑n = Submodule.span R ↑(Finset.image (fun n => Polynomial.X ^ n) (Finset.range (n + 1)))
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>f : R[X]<GOAL>f ∈ Polynomial.degreeLT R n ↔ f.degree < ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>m n : ℕ<VAR>H : m ≤ n<GOAL>Polynomial.degreeLT R m ≤ Polynomial.degreeLT R n
<VAR>R : Type u<VAR>Semiring R<VAR>DecidableEq R<VAR>n : ℕ<GOAL>Polynomial.degreeLT R n = Submodule.span R ↑(Finset.image (fun n => Polynomial.X ^ n) (Finset.range n))
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>p : R[X]<VAR>hp : p ∈ Polynomial.degreeLT R n<GOAL>(Polynomial.degreeLTEquiv R n) ⟨p, hp⟩ = 0 ↔ p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>p : R[X]<VAR>hp : p ∈ Polynomial.degreeLT R n<VAR>x : R<GOAL>Polynomial.eval x p = ∑ i : Fin n, (Polynomial.degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>Polynomial.degreeLT R (n + 1) = Polynomial.degreeLE R ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>s : Set R[X]<VAR>p : R[X]<VAR>hs : s.Nonempty<VAR>hp : p ∈ Submodule.span R s<GOAL>∃ p' ∈ s, p.degree ≤ p'.degree
<VAR>R : Type u<VAR>Semiring R<VAR>s : Set R[X]<VAR>s_fin : s.Finite<VAR>hs : s.Nonempty<GOAL>∃ p' ∈ s, ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree
<VAR>R : Type u<VAR>Semiring R<VAR>s : Set R[X]<VAR>s_fin : s.Finite<GOAL>∃ n, Submodule.span R s ≤ Polynomial.degreeLE R ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>s : Set R[X]<VAR>s_fin : s.Finite<GOAL>∃ n, Submodule.span R s ≤ Polynomial.degreeLT R n
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<GOAL>¬Module.Finite R R[X]
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.coeffs 0 = ∅
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>c : R<GOAL>c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.coeffs 1 ⊆ {1}
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : p.coeff n ≠ 0<GOAL>p.coeff n ∈ p.coeffs
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>(∑ i ∈ Finset.range n, Polynomial.X ^ i).comp (Polynomial.X + 1) = ∑ i ∈ Finset.range n, ↑(n.choose (i + 1)) * Polynomial.X ^ i
<VAR>R : Type u<VAR>Semiring R<VAR>P : R[X]<VAR>hP : P.Monic<VAR>hdeg : 0 < P.natDegree<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(∑ i ∈ Finset.range n, P ^ i).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>P : R[X]<VAR>hP : P.Monic<VAR>hdeg : 0 < P.degree<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(∑ i ∈ Finset.range n, P ^ i).Monic
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(∑ i ∈ Finset.range n, Polynomial.X ^ i).Monic
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>↑(p.restriction.coeff n) = p.coeff n
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>p.restriction.support = p.support
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<GOAL>Polynomial.map (algebraMap (↥(Subring.closure ↑p.coeffs)) R) p.restriction = p
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>p.restriction.degree = p.degree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>p.restriction.natDegree = p.natDegree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>p.restriction.Monic ↔ p.Monic
<VAR>R : Type u<VAR>Ring R<GOAL>Polynomial.restriction 0 = 0
<VAR>R : Type u<VAR>Ring R<GOAL>Polynomial.restriction 1 = 1
<VAR>R : Type u<VAR>S : Type u_1<VAR>Ring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<GOAL>Polynomial.eval₂ f x p = Polynomial.eval₂ (f.comp (Subring.closure ↑p.coeffs).subtype) x p.restriction
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<VAR>n : ℕ<GOAL>↑((p.toSubring T hp).coeff n) = p.coeff n
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<GOAL>(p.toSubring T hp).support = p.support
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<GOAL>(p.toSubring T hp).degree = p.degree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<GOAL>(p.toSubring T hp).natDegree = p.natDegree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<GOAL>(p.toSubring T hp).Monic ↔ p.Monic
<VAR>R : Type u<VAR>Ring R<VAR>T : Subring R<GOAL>Polynomial.toSubring 0 T ⋯ = 0
<VAR>R : Type u<VAR>Ring R<VAR>T : Subring R<GOAL>Polynomial.toSubring 1 T ⋯ = 1
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<GOAL>Polynomial.map T.subtype (p.toSubring T hp) = p
<VAR>R : Type u<VAR>Ring R<VAR>T : Subring R<VAR>p : (↥T)[X]<VAR>n : ℕ<GOAL>(Polynomial.ofSubring T p).coeff n = ↑(p.coeff n)
<VAR>R : Type u<VAR>Ring R<VAR>T : Subring R<VAR>p : (↥T)[X]<GOAL>↑(Polynomial.ofSubring T p).coeffs ⊆ ↑T
<VAR>R : Type u<VAR>CommRing R<VAR>q : R[X]<VAR>hq : q.Monic<VAR>p : R[X]<GOAL>p ∈ LinearMap.ker q.modByMonicHom ↔ q ∣ p
<VAR>R : Type u<VAR>CommRing R<VAR>q : R[X]<VAR>hq : q.Monic<GOAL>LinearMap.ker q.modByMonicHom = Submodule.restrictScalars R (Ideal.span {q})
<VAR>R : Type u<VAR>Semiring R<VAR>I : Ideal R[X]<VAR>x : R[X]<GOAL>x ∈ I.ofPolynomial ↔ x ∈ I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R[X]<VAR>p : R[X]<VAR>hp : ∀ (n : ℕ), p.coeff n ∈ Ideal.comap Polynomial.C I<GOAL>p ∈ I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>f : R[X]<GOAL>f ∈ Ideal.map Polynomial.C I ↔ ∀ (n : ℕ), f.coeff n ∈ I
<VAR>R : Type u<VAR>S : Type u_1<VAR>CommSemiring R<VAR>Semiring S<VAR>f : R →+* S<GOAL>LinearMap.ker (Polynomial.mapRingHom f).toSemilinearMap = Ideal.map Polynomial.C (RingHom.ker f)
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R[X]<VAR>n : ℕ<VAR>x : R<GOAL>x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R[X]<VAR>x : R<GOAL>x ∈ I.leadingCoeffNth 0 ↔ Polynomial.C x ∈ I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R[X]<VAR>m n : ℕ<VAR>H : m ≤ n<GOAL>I.leadingCoeffNth m ≤ I.leadingCoeffNth n
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R[X]<VAR>x : R<GOAL>x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → R[X]<VAR>I : Ideal R<VAR>n : ι → ℕ<VAR>h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)<VAR>k : ℕ<GOAL>(s.prod f).coeff k ∈ I ^ (s.sum n - k)
<VAR>R : Type u<VAR>Ring R<GOAL>¬IsField R[X]
<VAR>R : Type u<VAR>Ring R<VAR>hR : IsField R<VAR>I : Ideal R[X]<VAR>hI : I.IsMaximal<VAR>x : R<VAR>hx : Polynomial.C x ∈ I<GOAL>x = 0
<VAR>R : Type u<VAR>CommRing R<VAR>P : Ideal R<GOAL>(Ideal.map Polynomial.C P).IsPrime ↔ P.IsPrime
<VAR>R : Type u<VAR>CommRing R<VAR>P : Ideal R<VAR>H : P.IsPrime<GOAL>(Ideal.map Polynomial.C P).IsPrime
<VAR>R : Type u<VAR>CommRing R<VAR>IsNoetherianRing R<VAR>I : Ideal R[X]<VAR>n : ℕ<GOAL>(I.degreeLE ↑n).FG
<VAR>R : Type u<VAR>CommRing R<VAR>r : R<GOAL>Prime (Polynomial.C r) ↔ Prime r
<VAR>R : Type u<VAR>σ : Type v<VAR>r : R<VAR>CommRing R<VAR>Fintype σ<GOAL>Prime (MvPolynomial.C r) ↔ Prime r
<VAR>R : Type u<VAR>σ : Type v<VAR>CommRing R<VAR>r : R<GOAL>Prime (MvPolynomial.C r) ↔ Prime r
<VAR>R : Type u<VAR>σ : Type v<VAR>CommRing R<VAR>s : Set σ<VAR>p : MvPolynomial (↑s) R<GOAL>Prime ((MvPolynomial.rename Subtype.val) p) ↔ Prime p
<VAR>R : Type u<VAR>CommRing R<VAR>inst : IsNoetherianRing R<GOAL>IsNoetherianRing R[X]
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>WfDvdMonoid R<VAR>f : R[X]<VAR>hf : 0 < f.degree<GOAL>∃ g, Irreducible g ∧ g ∣ f
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>WfDvdMonoid R<VAR>f : R[X]<VAR>hf : 0 < f.natDegree<GOAL>∃ g, Irreducible g ∧ g ∣ f
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>WfDvdMonoid R<VAR>f : R[X]<VAR>hf : f.natDegree ≠ 0<GOAL>∃ g, Irreducible g ∧ g ∣ f
<VAR>R : Type u<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>v : M<GOAL>(LinearIndependent R fun n => (f ^ n) v) ↔ ∀ (p : R[X]), ((Polynomial.aeval f) p) v = 0 → p = 0
<VAR>R : Type u<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<GOAL>Disjoint (LinearMap.ker ((Polynomial.aeval f) p)) (LinearMap.ker ((Polynomial.aeval f) q))
<VAR>R : Type u<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<GOAL>LinearMap.range ((Polynomial.aeval f) p) ⊔ LinearMap.range ((Polynomial.aeval f) q) = ⊤
<VAR>R : Type u<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<GOAL>LinearMap.ker ((Polynomial.aeval f) p) ⊔ LinearMap.ker ((Polynomial.aeval f) q) ≤ LinearMap.ker ((Polynomial.aeval f) (p * q))
<VAR>R : Type u<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<GOAL>LinearMap.ker ((Polynomial.aeval f) p) ⊔ LinearMap.ker ((Polynomial.aeval f) q) = LinearMap.ker ((Polynomial.aeval f) (p * q))
<VAR>σ : Type v<VAR>R : Type u_2<VAR>CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<GOAL>((MvPolynomial.aeval f) F).natDegree ≤ m * n
<VAR>R : Type u<VAR>CommRing R<VAR>IsNoetherianRing R<GOAL>IsNoetherianRing (MvPolynomial (Fin 0) R)
<VAR>R : Type u<VAR>CommRing R<VAR>IsNoetherianRing R<VAR>n : ℕ<GOAL>IsNoetherianRing (MvPolynomial (Fin n) R)
<VAR>R : Type u<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>n : ℕ<GOAL>NoZeroDivisors (MvPolynomial (Fin n) R)
<VAR>R : Type u<VAR>σ : Type v<VAR>CommSemiring R<VAR>Finite σ<VAR>NoZeroDivisors R<GOAL>NoZeroDivisors (MvPolynomial σ R)
<VAR>R : Type u<VAR>σ : Type v<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Finite σ<VAR>ϕ : MvPolynomial σ R →+* S<VAR>p : MvPolynomial σ R<GOAL>ϕ p = MvPolynomial.eval₂ (ϕ.comp MvPolynomial.C) (fun s => ϕ (MvPolynomial.X s)) p
<VAR>R : Type u<VAR>σ : Type v<VAR>CommRing R<VAR>I : Ideal (MvPolynomial σ R)<VAR>p : MvPolynomial σ R<VAR>hcoe : ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p ∈ Ideal.comap MvPolynomial.C I<GOAL>p ∈ I
<VAR>R : Type u<VAR>σ : Type v<VAR>CommRing R<VAR>I : Ideal R<VAR>f : MvPolynomial σ R<GOAL>f ∈ Ideal.map MvPolynomial.C I ↔ ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m f ∈ I
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<GOAL>RingHom.ker (MvPolynomial.map f) = Ideal.map MvPolynomial.C (RingHom.ker f)
<VAR>σ : Type v<VAR>D : Type u<VAR>CommRing D<VAR>IsDomain D<VAR>UniqueFactorizationMonoid D<VAR>Fintype σ<GOAL>UniqueFactorizationMonoid (MvPolynomial σ D)
<VAR>F : Type u_2<VAR>Field F<VAR>f : F[X]<VAR>hu : ¬IsUnit f<GOAL>∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>P : ℕ → Prop<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(WittVector.select P x).coeff n = (MvPolynomial.aeval x.coeff) (WittVector.selectPoly P n)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>P : ℕ → Prop<VAR>x : 𝕎 R<GOAL>WittVector.select P x + WittVector.select (fun i => ¬P i) x = x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : 𝕎 R<VAR>h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0<GOAL>(x + y).coeff n = x.coeff n + y.coeff n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>WittVector.init n x + WittVector.tail n x = x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>WittVector.init n (WittVector.init n x) = WittVector.init n x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : 𝕎 R<VAR>n : ℕ<GOAL>WittVector.init n (x + y) = WittVector.init n (WittVector.init n x + WittVector.init n y)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : 𝕎 R<VAR>n : ℕ<GOAL>WittVector.init n (x * y) = WittVector.init n (WittVector.init n x * WittVector.init n y)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>WittVector.init n (-x) = WittVector.init n (-WittVector.init n x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : 𝕎 R<VAR>n : ℕ<GOAL>WittVector.init n (x - y) = WittVector.init n (WittVector.init n x - WittVector.init n y)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>m : ℕ<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>WittVector.init n (m • x) = WittVector.init n (m • WittVector.init n x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>m : ℤ<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>WittVector.init n (m • x) = WittVector.init n (m • WittVector.init n x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>m : ℕ<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>WittVector.init n (x ^ m) = WittVector.init n (WittVector.init n x ^ m)
<VAR>p n : ℕ<GOAL>WittVector.IsPoly p fun x x_1 => WittVector.init n
<VAR>p n : ℕ<VAR>R : Type u_1<VAR>x y : TruncatedWittVector p n R<VAR>h : ∀ (i : Fin n), TruncatedWittVector.coeff i x = TruncatedWittVector.coeff i y<GOAL>x = y
<VAR>p n : ℕ<VAR>R : Type u_1<VAR>x y : TruncatedWittVector p n R<GOAL>x = y ↔ ∀ (i : Fin n), TruncatedWittVector.coeff i x = TruncatedWittVector.coeff i y
<VAR>p n : ℕ<VAR>R : Type u_1<VAR>x : Fin n → R<VAR>i : Fin n<GOAL>TruncatedWittVector.coeff i (TruncatedWittVector.mk p x) = x i
<VAR>p n : ℕ<VAR>R : Type u_1<VAR>x : TruncatedWittVector p n R<GOAL>(TruncatedWittVector.mk p fun i => TruncatedWittVector.coeff i x) = x
<VAR>p n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : TruncatedWittVector p n R<VAR>i : Fin n<GOAL>x.out.coeff ↑i = TruncatedWittVector.coeff i x
<VAR>p n : ℕ<VAR>R : Type u_1<VAR>CommRing R<GOAL>Function.Injective TruncatedWittVector.out
<VAR>p n : ℕ<VAR>R : Type u_1<VAR>x : 𝕎 R<VAR>i : Fin n<GOAL>TruncatedWittVector.coeff i (WittVector.truncateFun n x) = x.coeff ↑i
<VAR>p n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : 𝕎 R<GOAL>(WittVector.truncateFun n x).out = WittVector.init n x
<VAR>p n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : TruncatedWittVector p n R<GOAL>WittVector.truncateFun n x.out = x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>i : Fin n<GOAL>TruncatedWittVector.coeff i 0 = 0
<VAR>p n : ℕ<VAR>R : Type u_1<VAR>CommRing R<GOAL>Function.Surjective (WittVector.truncateFun n)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<GOAL>WittVector.truncateFun n 0 = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<GOAL>WittVector.truncateFun n 1 = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : 𝕎 R<GOAL>WittVector.truncateFun n (x + y) = WittVector.truncateFun n x + WittVector.truncateFun n y
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : 𝕎 R<GOAL>WittVector.truncateFun n (x * y) = WittVector.truncateFun n x * WittVector.truncateFun n y
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : 𝕎 R<GOAL>WittVector.truncateFun n (-x) = -WittVector.truncateFun n x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : 𝕎 R<GOAL>WittVector.truncateFun n (x - y) = WittVector.truncateFun n x - WittVector.truncateFun n y
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>m : ℕ<VAR>x : 𝕎 R<GOAL>WittVector.truncateFun n (m • x) = m • WittVector.truncateFun n x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>m : ℤ<VAR>x : 𝕎 R<GOAL>WittVector.truncateFun n (m • x) = m • WittVector.truncateFun n x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : 𝕎 R<VAR>m : ℕ<GOAL>WittVector.truncateFun n (x ^ m) = WittVector.truncateFun n x ^ m
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>m : ℕ<GOAL>WittVector.truncateFun n ↑m = ↑m
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>m : ℤ<GOAL>WittVector.truncateFun n ↑m = ↑m
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<GOAL>Function.Surjective ⇑(WittVector.truncate n)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : 𝕎 R<VAR>i : Fin n<GOAL>TruncatedWittVector.coeff i ((WittVector.truncate n) x) = x.coeff ↑i
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : 𝕎 R<GOAL>x ∈ RingHom.ker (WittVector.truncate n) ↔ ∀ i < n, x.coeff i = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>f : ℕ → R<GOAL>(WittVector.truncate n) { coeff := f } = TruncatedWittVector.mk p fun k => f ↑k
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>(TruncatedWittVector.truncate hm).comp (WittVector.truncate m) = WittVector.truncate n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>x : 𝕎 R<GOAL>(TruncatedWittVector.truncate hm) ((WittVector.truncate m) x) = (WittVector.truncate n) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>n₁ n₂ n₃ : ℕ<VAR>h1 : n₁ ≤ n₂<VAR>h2 : n₂ ≤ n₃<VAR>x : TruncatedWittVector p n₃ R<GOAL>(TruncatedWittVector.truncate h1) ((TruncatedWittVector.truncate h2) x) = (TruncatedWittVector.truncate ⋯) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>n₁ n₂ n₃ : ℕ<VAR>h1 : n₁ ≤ n₂<VAR>h2 : n₂ ≤ n₃<GOAL>(TruncatedWittVector.truncate h1).comp (TruncatedWittVector.truncate h2) = TruncatedWittVector.truncate ⋯
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>Function.Surjective ⇑(TruncatedWittVector.truncate hm)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>i : Fin n<VAR>x : TruncatedWittVector p m R<GOAL>TruncatedWittVector.coeff i ((TruncatedWittVector.truncate hm) x) = TruncatedWittVector.coeff (Fin.castLE hm i) x
<VAR>p n : ℕ<VAR>R : Type u_2<VAR>Fintype R<GOAL>Fintype.card (TruncatedWittVector p n R) = Fintype.card R ^ n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<GOAL>⨅ i, RingHom.ker (WittVector.truncate i) = ⊥
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<VAR>s : S<GOAL>(WittVector.truncate n) (WittVector.liftFun f s) = (f n) s
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<VAR>s : S<GOAL>(WittVector.truncate n) ((WittVector.lift f f_compat) s) = (f n) s
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<GOAL>(WittVector.truncate n).comp (WittVector.lift f f_compat) = f n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<VAR>g : S →+* 𝕎 R<VAR>g_compat : ∀ (k : ℕ), (WittVector.truncate k).comp g = f k<GOAL>WittVector.lift f f_compat = g
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>Semiring S<VAR>g : S →+* 𝕎 R<VAR>k : ℕ<GOAL>↑(WittVector.liftEquiv.symm g) k = (WittVector.truncate k).comp g
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>Semiring S<VAR>f : { f // ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁ }<GOAL>WittVector.liftEquiv f = WittVector.lift ↑f ⋯
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>Semiring S<VAR>g₁ g₂ : S →+* 𝕎 R<VAR>h : ∀ (k : ℕ), (WittVector.truncate k).comp g₁ = (WittVector.truncate k).comp g₂<GOAL>g₁ = g₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<GOAL>(Algebra.trace R S) x = (LinearMap.trace R S) ((Algebra.lmul R S) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)<GOAL>Algebra.trace R S = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>ι : Type w<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R S<VAR>s : S<GOAL>(Algebra.trace R S) s = ((Algebra.leftMulMatrix b) s).trace
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>ι : Type w<VAR>Fintype ι<VAR>b : Basis ι R S<VAR>x : R<GOAL>(Algebra.trace R S) ((algebraMap R S) x) = Fintype.card ι • x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>StrongRankCondition R<VAR>Module.Free R S<VAR>x : R<GOAL>(Algebra.trace R S) ((algebraMap R S) x) = FiniteDimensional.finrank R S • x