ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>SMulZeroClass S R<VAR>a : S<VAR>n : ℕ<VAR>b : R<GOAL>a • (Polynomial.monomial n) b = (Polynomial.monomial n) (a • b)
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>Function.Injective ⇑(Polynomial.monomial n)
<VAR>R : Type u<VAR>Semiring R<VAR>t : R<VAR>n : ℕ<GOAL>(Polynomial.monomial n) t = 0 ↔ t = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>(p + q).support ⊆ p.support ∪ q.support
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.monomial 0) a = Polynomial.C a
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.C a).toFinsupp = AddMonoidAlgebra.single 0 a
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.C 0 = 0
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.C 1 = 1
<VAR>R : Type u<VAR>a b : R<VAR>Semiring R<GOAL>Polynomial.C (a * b) = Polynomial.C a * Polynomial.C b
<VAR>R : Type u<VAR>a b : R<VAR>Semiring R<GOAL>Polynomial.C (a + b) = Polynomial.C a + Polynomial.C b
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>SMulZeroClass S R<VAR>s : S<VAR>r : R<GOAL>s • Polynomial.C r = Polynomial.C (s • r)
<VAR>R : Type u<VAR>a : R<VAR>n : ℕ<VAR>Semiring R<GOAL>Polynomial.C (a ^ n) = Polynomial.C a ^ n
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>Polynomial.C ↑n = ↑n
<VAR>R : Type u<VAR>a b : R<VAR>n : ℕ<VAR>Semiring R<GOAL>Polynomial.C a * (Polynomial.monomial n) b = (Polynomial.monomial n) (a * b)
<VAR>R : Type u<VAR>a b : R<VAR>n : ℕ<VAR>Semiring R<GOAL>(Polynomial.monomial n) a * Polynomial.C b = (Polynomial.monomial n) (a * b)
<VAR>R : Type u<VAR>Semiring R<GOAL>(Polynomial.monomial 1) 1 = Polynomial.X
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>(Polynomial.monomial n) 1 = Polynomial.X ^ n
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.X.toFinsupp = Finsupp.single 1 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>Polynomial.X * p = p * Polynomial.X
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>Polynomial.X ^ n * p = p * Polynomial.X ^ n
<VAR>R : Type u<VAR>Semiring R<VAR>r : R<GOAL>Polynomial.X * Polynomial.C r = Polynomial.C r * Polynomial.X
<VAR>R : Type u<VAR>Semiring R<VAR>r : R<VAR>n : ℕ<GOAL>Polynomial.X ^ n * Polynomial.C r = Polynomial.C r * Polynomial.X ^ n
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>p * Polynomial.X ^ n * q = p * q * Polynomial.X ^ n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>r : R<GOAL>p * Polynomial.X ^ n * Polynomial.C r = p * Polynomial.C r * Polynomial.X ^ n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>Commute Polynomial.X p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>Commute (Polynomial.X ^ n) p
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>r : R<GOAL>(Polynomial.monomial n) r * Polynomial.X = (Polynomial.monomial (n + 1)) r
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>r : R<VAR>k : ℕ<GOAL>(Polynomial.monomial n) r * Polynomial.X ^ k = (Polynomial.monomial (n + k)) r
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>r : R<GOAL>Polynomial.X * (Polynomial.monomial n) r = (Polynomial.monomial (n + 1)) r
<VAR>R : Type u<VAR>Semiring R<VAR>k n : ℕ<VAR>r : R<GOAL>Polynomial.X ^ k * (Polynomial.monomial n) r = (Polynomial.monomial (n + k)) r
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[ℕ]<GOAL>{ toFinsupp := p }.coeff = ⇑p
<VAR>R : Type u<VAR>Semiring R<GOAL>Function.Injective Polynomial.coeff
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>p.coeff = q.coeff ↔ p = q
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<VAR>i : ℕ<GOAL>f.toFinsupp i = f.coeff i
<VAR>R : Type u<VAR>a : R<VAR>m n : ℕ<VAR>Semiring R<GOAL>((Polynomial.monomial n) a).coeff m = if n = m then a else 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>Polynomial.coeff 0 n = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>Polynomial.coeff 1 n = if n = 0 then 1 else 0
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.coeff 1 0 = 1
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.X.coeff 1 = 1
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.X.coeff 0 = 0
<VAR>R : Type u<VAR>a : R<VAR>n : ℕ<VAR>Semiring R<GOAL>((Polynomial.monomial (n + 1)) a).coeff 0 = 0
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<GOAL>Polynomial.X.coeff n = if 1 = n then 1 else 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>Polynomial.X.coeff n = 0
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<GOAL>n ∈ p.support ↔ p.coeff n ≠ 0
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<GOAL>n ∉ p.support ↔ p.coeff n = 0
<VAR>R : Type u<VAR>a : R<VAR>n : ℕ<VAR>Semiring R<GOAL>(Polynomial.C a).coeff n = if n = 0 then a else 0
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<GOAL>(Polynomial.C a).coeff 0 = a
<VAR>R : Type u<VAR>a : R<VAR>n : ℕ<VAR>Semiring R<VAR>h : n ≠ 0<GOAL>(Polynomial.C a).coeff n = 0
<VAR>R : Type u<VAR>Semiring R<VAR>r : R<VAR>n : ℕ<GOAL>(Polynomial.C r).coeff (n + 1) = 0
<VAR>R : Type u<VAR>m n : ℕ<VAR>Semiring R<GOAL>(↑m).coeff n = ↑(if n = 0 then m else 0)
<VAR>R : Type u<VAR>Semiring R<VAR>a : ℕ<VAR>a.AtLeastTwo<GOAL>(OfNat.ofNat a).coeff 0 = OfNat.ofNat a
<VAR>R : Type u<VAR>Semiring R<VAR>a n : ℕ<VAR>h : a.AtLeastTwo<GOAL>(OfNat.ofNat a).coeff (n + 1) = 0
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>n : ℕ<GOAL>Polynomial.C a * Polynomial.X ^ n = (Polynomial.monomial n) a
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>n : ℕ<GOAL>(Polynomial.C a * Polynomial.X ^ n).toFinsupp = Finsupp.single n a
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<GOAL>Polynomial.C a * Polynomial.X = (Polynomial.monomial 1) a
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.C a * Polynomial.X).toFinsupp = Finsupp.single 1 a
<VAR>R : Type u<VAR>Semiring R<GOAL>Function.Injective ⇑Polynomial.C
<VAR>R : Type u<VAR>a b : R<VAR>Semiring R<GOAL>Polynomial.C a = Polynomial.C b ↔ a = b
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<GOAL>Polynomial.C a = 0 ↔ a = 0
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<GOAL>Polynomial.C a ≠ 0 ↔ a ≠ 0
<VAR>R : Type u<VAR>Semiring R<GOAL>Subsingleton R[X] ↔ Subsingleton R
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p ≠ q<GOAL>Nontrivial R
<VAR>R : Type u<VAR>Semiring R<GOAL>(∀ (f g : R[X]), f = g) ↔ ∀ (a b : R), a = b
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>(∀ (n : ℕ), p.coeff n = q.coeff n) → p = q
<VAR>R : Type u<VAR>Semiring R<GOAL>AddSubmonoid.closure {p | ∃ n a, p = (Polynomial.monomial n) a} = ⊤
<VAR>R : Type u<VAR>Semiring R<VAR>M : Type u_1<VAR>AddMonoid M<VAR>f g : R[X] →+ M<VAR>h : ∀ (n : ℕ) (a : R), f ((Polynomial.monomial n) a) = g ((Polynomial.monomial n) a)<GOAL>f = g
<VAR>R : Type u<VAR>Semiring R<VAR>M : Type u_1<VAR>AddMonoid M<VAR>f g : R[X] →+ M<VAR>h : ∀ (n : ℕ), f.comp (Polynomial.monomial n).toAddMonoidHom = g.comp (Polynomial.monomial n).toAddMonoidHom<GOAL>f = g
<VAR>R : Type u<VAR>Semiring R<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : R[X] →ₗ[R] M<VAR>h : ∀ (n : ℕ), f ∘ₗ Polynomial.monomial n = g ∘ₗ Polynomial.monomial n<GOAL>f = g
<VAR>R : Type u<VAR>Semiring R<VAR>h : 0 = 1<VAR>p : R[X]<GOAL>p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<VAR>H : a ≠ 0<GOAL>((Polynomial.monomial n) a).support = {n}
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<GOAL>((Polynomial.monomial n) a).support ⊆ {n}
<VAR>R : Type u<VAR>Semiring R<VAR>c : R<VAR>h : c ≠ 0<GOAL>(Polynomial.C c * Polynomial.X).support = {1}
<VAR>R : Type u<VAR>Semiring R<VAR>c : R<GOAL>(Polynomial.C c * Polynomial.X).support ⊆ {1}
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>c : R<VAR>h : c ≠ 0<GOAL>(Polynomial.C c * Polynomial.X ^ n).support = {n}
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>c : R<GOAL>(Polynomial.C c * Polynomial.X ^ n).support ⊆ {n}
<VAR>R : Type u<VAR>Semiring R<VAR>k m : ℕ<VAR>x y : R<GOAL>(Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support ⊆ {k, m}
<VAR>R : Type u<VAR>Semiring R<VAR>k m n : ℕ<VAR>x y z : R<GOAL>(Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support ⊆ {k, m, n}
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>Polynomial.X ^ n = (Polynomial.monomial n) 1
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).toFinsupp = Finsupp.single n 1
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>n : ℕ<GOAL>a • Polynomial.X ^ n = (Polynomial.monomial n) a
<VAR>R : Type u<VAR>Semiring R<VAR>H : ¬1 = 0<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).support = {n}
<VAR>R : Type u<VAR>Semiring R<VAR>H : 1 = 0<GOAL>Polynomial.X.support = ∅
<VAR>R : Type u<VAR>Semiring R<VAR>H : ¬1 = 0<GOAL>Polynomial.X.support = {1}
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>ha : a ≠ 0<VAR>i j : ℕ<GOAL>(Polynomial.monomial i) a = (Polynomial.monomial j) a ↔ i = j
<VAR>R : Type u<VAR>Semiring R<VAR>k l m n : ℕ<VAR>u v : R<VAR>hu : u ≠ 0<VAR>hv : v ≠ 0<GOAL>Polynomial.C u * Polynomial.X ^ k + Polynomial.C v * Polynomial.X ^ l = Polynomial.C u * Polynomial.X ^ m + Polynomial.C v * Polynomial.X ^ n ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>p : R[X]<GOAL>↑n * p = n • p
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>AddCommMonoid S<VAR>p : R[X]<VAR>f : ℕ → R → S<GOAL>p.sum f = ∑ n ∈ p.support, f n (p.coeff n)
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>AddCommMonoid S<VAR>p : R[X]<VAR>f : ℕ → R → S<VAR>hf : ∀ (i : ℕ), f i 0 = 0<VAR>s : Finset ℕ<VAR>hs : p.support ⊆ s<GOAL>p.sum f = ∑ n ∈ s, f n (p.coeff n)
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>p * q = ∑ i ∈ p.support, q.sum fun j a => (Polynomial.monomial (i + j)) (p.coeff i * a)
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>AddCommMonoid S<VAR>f : ℕ → R → S<GOAL>Polynomial.sum 0 f = 0
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>AddCommMonoid S<VAR>n : ℕ<VAR>a : R<VAR>f : ℕ → R → S<VAR>hf : f n 0 = 0<GOAL>((Polynomial.monomial n) a).sum f = f n a
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>β : Type u_1<VAR>AddCommMonoid β<VAR>f : ℕ → R → β<VAR>h : f 0 0 = 0<GOAL>(Polynomial.C a).sum f = f 0 a
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>AddCommMonoid S<VAR>f : ℕ → R → S<VAR>hf : f 1 0 = 0<GOAL>Polynomial.X.sum f = f 1 1
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>AddCommMonoid S<VAR>p q : R[X]<VAR>f : ℕ → R → S<VAR>hf : ∀ (i : ℕ), f i 0 = 0<VAR>h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂<GOAL>(p + q).sum f = p.sum f + q.sum f
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>AddCommMonoid S<VAR>p : R[X]<VAR>f g : ℕ → R → S<GOAL>p.sum (f + g) = p.sum f + p.sum g
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>AddCommMonoid S<VAR>p : R[X]<VAR>f g : ℕ → R → S<GOAL>(p.sum fun n x => f n x + g n x) = p.sum f + p.sum g
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>AddCommMonoid S<VAR>p : R[X]<VAR>b : R<VAR>f : ℕ → R → S<VAR>hf : ∀ (i : ℕ), f i 0 = 0<GOAL>(b • p).sum f = p.sum fun n a => f n (b * a)
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>T : Type u_2<VAR>DistribSMul T R<VAR>AddCommMonoid S<VAR>p : R[X]<VAR>b : T<VAR>f : ℕ → R → S<VAR>hf : ∀ (i : ℕ), f i 0 = 0<GOAL>(b • p).sum f = p.sum fun n a => f n (b • a)
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>T : Type u_2<VAR>AddCommMonoid S<VAR>DistribSMul T S<VAR>p : R[X]<VAR>b : T<VAR>f : ℕ → R → S<GOAL>b • p.sum f = p.sum fun n a => b • f n a
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>(p.sum fun n a => (Polynomial.monomial n) a) = p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>(p.sum fun n a => Polynomial.C a * Polynomial.X ^ n) = p
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>∀ (x : R[X]), Polynomial.erase n x = match x with | { toFinsupp := p } => { toFinsupp := Finsupp.erase n p }
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(Polynomial.erase n p).toFinsupp = Finsupp.erase n p.toFinsupp
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[ℕ]<VAR>n : ℕ<GOAL>{ toFinsupp := Finsupp.erase n p } = Polynomial.erase n { toFinsupp := p }
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(Polynomial.erase n p).support = p.support.erase n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(Polynomial.monomial n) (p.coeff n) + Polynomial.erase n p = p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n i : ℕ<GOAL>(Polynomial.erase n p).coeff i = if i = n then 0 else p.coeff i
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>Polynomial.erase n 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<GOAL>Polynomial.erase n ((Polynomial.monomial n) a) = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(Polynomial.erase n p).coeff n = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n i : ℕ<VAR>h : i ≠ n<GOAL>(Polynomial.erase n p).coeff i = p.coeff i
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>(p.update n a).coeff = Function.update p.coeff n a
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>a : R<VAR>i : ℕ<GOAL>(p.update n a).coeff i = if i = n then a else p.coeff i
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>(p.update n a).coeff n = a
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>a : R<VAR>i : ℕ<VAR>h : i ≠ n<GOAL>(p.update n a).coeff i = p.coeff i
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>p.update n 0 = Polynomial.erase n p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>a : R<VAR>Decidable (a = 0)<GOAL>(p.update n a).support = if a = 0 then p.support.erase n else insert n p.support
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p.update n 0).support = p.support.erase n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>a : R<VAR>ha : a ≠ 0<GOAL>(p.update n a).support = insert n p.support
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(-p).coeff n = -p.coeff n
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(p - q).coeff n = p.coeff n - q.coeff n
<VAR>R : Type u<VAR>Ring R<VAR>n : ℕ<VAR>a : R<GOAL>(Polynomial.monomial n) (-a) = -(Polynomial.monomial n) a
<VAR>R : Type u<VAR>a b : R<VAR>Ring R<VAR>n : ℕ<GOAL>(Polynomial.monomial n) (a - b) = (Polynomial.monomial n) a - (Polynomial.monomial n) b
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>(-p).support = p.support
<VAR>R : Type u<VAR>Ring R<VAR>n : ℤ<GOAL>Polynomial.C ↑n = ↑n
<VAR>R : Type u<VAR>a : R<VAR>Ring R<GOAL>Polynomial.C (-a) = -Polynomial.C a
<VAR>R : Type u<VAR>a b : R<VAR>Ring R<GOAL>Polynomial.C (a - b) = Polynomial.C a - Polynomial.C b
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<GOAL>Polynomial.X ≠ 0
<VAR>R : Type u<VAR>DivisionSemiring R<VAR>q : ℚ≥0<VAR>f : R[X]<GOAL>q • f = Polynomial.C ↑q * f
<VAR>R : Type u<VAR>DivisionRing R<VAR>a : ℚ<VAR>f : R[X]<GOAL>a • f = Polynomial.C ↑a * f
<VAR>R : Type u<VAR>Semiring R<GOAL>Nontrivial R[X] ↔ Nontrivial R
<VAR>M : Type u_1<VAR>Monoid M<VAR>R : Type u_2<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>m : M<GOAL>HSMul.hSMul m = Polynomial.map (MulSemiringAction.toRingHom M R m)
<VAR>M : Type u_1<VAR>Monoid M<VAR>R : Type u_2<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>m : M<GOAL>m • Polynomial.X = Polynomial.X
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Type u_3<VAR>CommSemiring S<VAR>MulSemiringAction M S<VAR>m : M<VAR>f : S[X]<VAR>x : S<GOAL>Polynomial.eval (m • x) (m • f) = m • Polynomial.eval x f
<VAR>S : Type u_3<VAR>CommSemiring S<VAR>G : Type u_4<VAR>Group G<VAR>MulSemiringAction G S<VAR>g : G<VAR>f : S[X]<VAR>x : S<GOAL>Polynomial.eval (g • x) f = g • Polynomial.eval x (g⁻¹ • f)
<VAR>S : Type u_3<VAR>CommSemiring S<VAR>G : Type u_4<VAR>Group G<VAR>MulSemiringAction G S<VAR>g : G<VAR>f : S[X]<VAR>x : S<GOAL>Polynomial.eval x (g • f) = g • Polynomial.eval (g⁻¹ • x) f
<VAR>G : Type u_2<VAR>Group G<VAR>Fintype G<VAR>R : Type u_3<VAR>CommRing R<VAR>MulSemiringAction G R<VAR>x : R<GOAL>(prodXSubSMul G R x).Monic
<VAR>G : Type u_2<VAR>Group G<VAR>Fintype G<VAR>R : Type u_3<VAR>CommRing R<VAR>MulSemiringAction G R<VAR>x : R<GOAL>Polynomial.eval x (prodXSubSMul G R x) = 0
<VAR>G : Type u_2<VAR>Group G<VAR>Fintype G<VAR>R : Type u_3<VAR>CommRing R<VAR>MulSemiringAction G R<VAR>x : R<VAR>g : G<GOAL>g • prodXSubSMul G R x = prodXSubSMul G R x
<VAR>G : Type u_2<VAR>Group G<VAR>Fintype G<VAR>R : Type u_3<VAR>CommRing R<VAR>MulSemiringAction G R<VAR>x : R<VAR>g : G<VAR>n : ℕ<GOAL>g • (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n
<VAR>M : Type u_1<VAR>Monoid M<VAR>P : Type u_2<VAR>CommSemiring P<VAR>MulSemiringAction M P<VAR>Q : Type u_3<VAR>CommSemiring Q<VAR>MulSemiringAction M Q<VAR>g : P →+*[M] Q<GOAL>⇑g.polynomial = Polynomial.map ↑g
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ Polynomial.lifts f ↔ ∃ q, Polynomial.map f q = p
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ Polynomial.lifts f ↔ p ∈ Set.range (Polynomial.map f)
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ Polynomial.lifts f ↔ p ∈ (Polynomial.mapRingHom f).rangeS
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ Polynomial.lifts f ↔ ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>r : R<GOAL>Polynomial.C (f r) ∈ Polynomial.lifts f
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>h : s ∈ Set.range ⇑f<GOAL>Polynomial.C s ∈ Polynomial.lifts f
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<GOAL>Polynomial.X ∈ Polynomial.lifts f
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>Polynomial.X ^ n ∈ Polynomial.lifts f
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>r : R<VAR>hp : p ∈ Polynomial.lifts f<GOAL>Polynomial.C (f r) * p ∈ Polynomial.lifts f
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>h : s ∈ Set.range ⇑f<GOAL>(Polynomial.monomial n) s ∈ Polynomial.lifts f
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>n : ℕ<VAR>h : p ∈ Polynomial.lifts f<GOAL>Polynomial.erase n p ∈ Polynomial.lifts f
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>hl : (Polynomial.monomial n) s ∈ Polynomial.lifts f<GOAL>∃ q, Polynomial.map f q = (Polynomial.monomial n) s ∧ q.degree = ((Polynomial.monomial n) s).degree
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>hlifts : p ∈ Polynomial.lifts f<GOAL>∃ q, Polynomial.map f q = p ∧ q.degree = p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>Nontrivial S<VAR>p : S[X]<VAR>hlifts : p ∈ Polynomial.lifts f<VAR>hp : p.Monic<GOAL>∃ q, Polynomial.map f q = p ∧ q.degree = p.degree ∧ q.Monic
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type v<VAR>Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>hlifts : p ∈ Polynomial.lifts f<VAR>hp : p.Monic<GOAL>∃ q, Polynomial.map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
<VAR>R : Type u<VAR>Ring R<VAR>S : Type v<VAR>Ring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ Polynomial.lifts f ↔ p ∈ Polynomial.liftsRing f
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type v<VAR>Semiring S<VAR>Algebra R S<VAR>p : R[X]<GOAL>(Polynomial.mapAlg R S) p = Polynomial.map (algebraMap R S) p
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type v<VAR>Semiring S<VAR>Algebra R S<VAR>p : S[X]<GOAL>p ∈ Polynomial.lifts (algebraMap R S) ↔ p ∈ (Polynomial.mapAlg R S).range
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type v<VAR>Semiring S<VAR>Algebra R S<VAR>p : S[X]<VAR>r : R<VAR>hp : p ∈ Polynomial.lifts (algebraMap R S)<GOAL>r • p ∈ Polynomial.lifts (algebraMap R S)
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(p + q).coeff n = p.coeff n + q.coeff n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>SMulZeroClass S R<VAR>r : S<VAR>p : R[X]<VAR>n : ℕ<GOAL>(r • p).coeff n = r • p.coeff n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>SMulZeroClass S R<VAR>r : S<VAR>p : R[X]<GOAL>(r • p).support ⊆ p.support
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>(p * q).support.card ≤ p.support.card * q.support.card
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>Semiring A<VAR>AddCommMonoid M<VAR>Module R A<VAR>Module R M<VAR>f : ℕ → A →ₗ[R] M<VAR>p : A[X]<GOAL>(Polynomial.lsum f) p = p.sum fun x x_1 => (f x) x_1
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>f : R[X]<GOAL>(Polynomial.lcoeff R n) f = f.coeff n
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → R[X]<VAR>n : ℕ<GOAL>(∑ b ∈ s, f b).coeff n = ∑ b ∈ s, (f b).coeff n
<VAR>R : Type u<VAR>Semiring R<VAR>l : List R[X]<VAR>n : ℕ<GOAL>l.sum.coeff n = (List.map (⇑(Polynomial.lcoeff R n)) l).sum
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type u_1<VAR>l : List ι<VAR>f : ι → R[X]<VAR>n : ℕ<GOAL>(List.map f l).sum.coeff n = (List.map (fun a => (f a).coeff n) l).sum
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>n : ℕ<VAR>f : ℕ → R → S[X]<GOAL>(p.sum f).coeff n = p.sum fun a b => (f a b).coeff n
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(p * q).coeff n = ∑ x ∈ Finset.antidiagonal n, p.coeff x.1 * q.coeff x.2
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>(p * q).coeff 0 = p.coeff 0 * q.coeff 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>Polynomial.constantCoeff p = p.coeff 0
<VAR>R : Type u<VAR>Semiring R<VAR>x : R<GOAL>IsUnit (Polynomial.C x) ↔ IsUnit x
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>(p * Polynomial.X).coeff 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>(Polynomial.X * p).coeff 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>x : R<VAR>k n : ℕ<GOAL>(Polynomial.C x * Polynomial.X ^ k).coeff n = if n = k then x else 0
<VAR>R : Type u<VAR>Semiring R<VAR>x : R<VAR>n : ℕ<GOAL>(Polynomial.C x * Polynomial.X).coeff n = if n = 1 then x else 0
<VAR>R : Type u<VAR>a : R<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<GOAL>(Polynomial.C a * p).coeff n = a * p.coeff n
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>f : R[X]<GOAL>Polynomial.C a * f = a • f
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>(p * Polynomial.C a).coeff n = p.coeff n * a
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>a k : ℕ<GOAL>(p * ↑a).coeff k = p.coeff k * ↑a
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>a k : ℕ<GOAL>(↑a * p).coeff k = ↑a * p.coeff k
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>a k : ℕ<VAR>a.AtLeastTwo<GOAL>(p * OfNat.ofNat a).coeff k = p.coeff k * OfNat.ofNat a
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>a k : ℕ<VAR>a.AtLeastTwo<GOAL>(OfNat.ofNat a * p).coeff k = OfNat.ofNat a * p.coeff k
<VAR>S : Type v<VAR>Ring S<VAR>p : S[X]<VAR>a : ℤ<VAR>k : ℕ<GOAL>(p * ↑a).coeff k = p.coeff k * ↑a
<VAR>S : Type v<VAR>Ring S<VAR>p : S[X]<VAR>a : ℤ<VAR>k : ℕ<GOAL>(↑a * p).coeff k = ↑a * p.coeff k
<VAR>R : Type u<VAR>Semiring R<VAR>k n : ℕ<GOAL>(Polynomial.X ^ k).coeff n = if n = k then 1 else 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).coeff n = 1
<VAR>R : Type u<VAR>Semiring R<VAR>k m : ℕ<VAR>hkm : k ≠ m<VAR>x y : R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support = {k, m}
<VAR>R : Type u<VAR>Semiring R<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>x y z : R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>(Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support = {k, m, n}
<VAR>R : Type u<VAR>Semiring R<VAR>k m : ℕ<VAR>h : k ≠ m<VAR>x y : R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support.card = 2
<VAR>R : Type u<VAR>Semiring R<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>x y z : R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>(Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support.card = 3
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n d : ℕ<GOAL>(p * Polynomial.X ^ n).coeff (d + n) = p.coeff d
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n d : ℕ<GOAL>(Polynomial.X ^ n * p).coeff (d + n) = p.coeff d
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n d : ℕ<GOAL>(p * Polynomial.X ^ n).coeff d = if n ≤ d then p.coeff (d - n) else 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n d : ℕ<GOAL>(Polynomial.X ^ n * p).coeff d = if n ≤ d then p.coeff (d - n) else 0