ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p * Polynomial.X).coeff (n + 1) = p.coeff n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(Polynomial.X * p).coeff (n + 1) = p.coeff n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n d : ℕ<VAR>r : R<GOAL>(p * (Polynomial.monomial n) r).coeff (d + n) = p.coeff d * r
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n d : ℕ<VAR>r : R<GOAL>((Polynomial.monomial n) r * p).coeff (d + n) = r * p.coeff d
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>d : ℕ<VAR>r : R<GOAL>(p * (Polynomial.monomial 0) r).coeff d = p.coeff d * r
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>d : ℕ<VAR>r : R<GOAL>((Polynomial.monomial 0) r * p).coeff d = r * p.coeff d
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>H : p * Polynomial.X ^ n = 0<GOAL>p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>IsRegular (Polynomial.X ^ n)
<VAR>R : Type u<VAR>Semiring R<GOAL>IsRegular Polynomial.X
<VAR>R : Type u<VAR>Semiring R<VAR>r : R<VAR>n k : ℕ<GOAL>((Polynomial.X + Polynomial.C r) ^ n).coeff k = r ^ (n - k) * ↑(n.choose k)
<VAR>R : Type u_1<VAR>Semiring R<VAR>n k : ℕ<GOAL>((Polynomial.X + 1) ^ n).coeff k = ↑(n.choose k)
<VAR>R : Type u_1<VAR>Semiring R<VAR>n k : ℕ<GOAL>((1 + Polynomial.X) ^ n).coeff k = ↑(n.choose k)
<VAR>R : Type u<VAR>Semiring R<VAR>r : R<VAR>φ : R[X]<GOAL>Polynomial.C r ∣ φ ↔ ∀ (i : ℕ), r ∣ φ.coeff i
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>a : R<GOAL>a • p = Polynomial.C a * p
<VAR>R : Type u_1<VAR>Ring R<VAR>p : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>p.update n a = p + Polynomial.C (a - p.coeff n) * Polynomial.X ^ n
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Semiring R<GOAL>(↑n).coeff 0 = ↑n
<VAR>m n : ℕ<VAR>R : Type u_1<VAR>Semiring R<VAR>CharZero R<GOAL>↑m = ↑n ↔ m = n
<VAR>i : ℤ<VAR>R : Type u_1<VAR>Ring R<GOAL>(↑i).coeff 0 = ↑i
<VAR>m n : ℤ<VAR>R : Type u_1<VAR>Ring R<VAR>CharZero R<GOAL>↑m = ↑n ↔ m = n
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.mirror 0 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<GOAL>((Polynomial.monomial n) a).mirror = (Polynomial.monomial n) a
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.C a).mirror = Polynomial.C a
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.X.mirror = Polynomial.X
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>p.mirror.natDegree = p.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>p.mirror.natTrailingDegree = p.natTrailingDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>n : ℕ<GOAL>p.mirror.coeff n = p.coeff ((Polynomial.revAt (p.natDegree + p.natTrailingDegree)) n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>Polynomial.eval 1 p.mirror = Polynomial.eval 1 p
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>p.mirror.mirror = p
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Function.Involutive Polynomial.mirror
<VAR>R : Type u_1<VAR>Semiring R<VAR>p q : Polynomial R<GOAL>p.mirror = q ↔ p = q.mirror
<VAR>R : Type u_1<VAR>Semiring R<VAR>p q : Polynomial R<GOAL>p.mirror = q.mirror ↔ p = q
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>p.mirror = 0 ↔ p = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>p.mirror.trailingCoeff = p.leadingCoeff
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>p.mirror.leadingCoeff = p.trailingCoeff
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>(p * p.mirror).coeff (p.natDegree + p.natTrailingDegree) = p.sum fun n x => x ^ 2
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>NoZeroDivisors R<GOAL>(p * p.mirror).natDegree = 2 * p.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>NoZeroDivisors R<GOAL>(p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
<VAR>R : Type u_1<VAR>Ring R<VAR>p : Polynomial R<GOAL>(-p).mirror = -p.mirror
<VAR>R : Type u_1<VAR>Ring R<VAR>p q : Polynomial R<VAR>NoZeroDivisors R<GOAL>(p * q).mirror = p.mirror * q.mirror
<VAR>R : Type u_1<VAR>Ring R<VAR>p : Polynomial R<VAR>NoZeroDivisors R<VAR>a : R<GOAL>(a • p).mirror = a • p.mirror
<VAR>R : Type u_1<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>f : Polynomial R<VAR>h1 : ¬IsUnit f<VAR>h2 : ∀ (k : Polynomial R), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror<VAR>h3 : IsRelPrime f f.mirror<GOAL>Irreducible f
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>Polynomial.derivative p = p.sum fun n a => Polynomial.C (a * ↑n) * Polynomial.X ^ (n - 1)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(Polynomial.derivative p).coeff n = p.coeff (n + 1) * (↑n + 1)
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.derivative 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>k : ℕ<GOAL>(⇑Polynomial.derivative)^[k] 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>n : ℕ<GOAL>Polynomial.derivative ((Polynomial.monomial n) a) = (Polynomial.monomial (n - 1)) (a * ↑n)
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>Polynomial.derivative (Polynomial.C a * Polynomial.X) = Polynomial.C a
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>n : ℕ<GOAL>Polynomial.derivative (Polynomial.C a * Polynomial.X ^ n) = Polynomial.C (a * ↑n) * Polynomial.X ^ (n - 1)
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>Polynomial.derivative (Polynomial.C a * Polynomial.X ^ 2) = Polynomial.C (a * 2) * Polynomial.X
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>Polynomial.derivative (Polynomial.X ^ n) = Polynomial.C ↑n * Polynomial.X ^ (n - 1)
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.derivative (Polynomial.X ^ 2) = Polynomial.C 2 * Polynomial.X
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>Polynomial.derivative (Polynomial.C a) = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.natDegree = 0<GOAL>Polynomial.derivative p = 0
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.derivative Polynomial.X = 1
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.derivative 1 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>f g : R[X]<GOAL>Polynomial.derivative (f + g) = Polynomial.derivative f + Polynomial.derivative g
<VAR>R : Type u<VAR>Semiring R<VAR>c : R<GOAL>Polynomial.derivative (Polynomial.X + Polynomial.C c) = 1
<VAR>R : Type u<VAR>ι : Type y<VAR>Semiring R<VAR>s : Finset ι<VAR>f : ι → R[X]<GOAL>Polynomial.derivative (∑ b ∈ s, f b) = ∑ b ∈ s, Polynomial.derivative (f b)
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>Monoid S<VAR>DistribMulAction S R<VAR>IsScalarTower S R R<VAR>s : S<VAR>p : R[X]<GOAL>Polynomial.derivative (s • p) = s • Polynomial.derivative p
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>Monoid S<VAR>DistribMulAction S R<VAR>IsScalarTower S R R<VAR>s : S<VAR>p : R[X]<VAR>k : ℕ<GOAL>(⇑Polynomial.derivative)^[k] (s • p) = s • (⇑Polynomial.derivative)^[k] p
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>p : R[X]<VAR>k : ℕ<GOAL>(⇑Polynomial.derivative)^[k] (Polynomial.C a * p) = Polynomial.C a * (⇑Polynomial.derivative)^[k] p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : n ∈ (Polynomial.derivative p).support<GOAL>n + 1 ∈ p.support
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p ≠ 0<GOAL>(Polynomial.derivative p).degree < p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>(Polynomial.derivative p).degree ≤ p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.natDegree ≠ 0<GOAL>(Polynomial.derivative p).natDegree < p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>(Polynomial.derivative p).natDegree ≤ p.natDegree - 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>k : ℕ<GOAL>((⇑Polynomial.derivative)^[k] p).natDegree ≤ p.natDegree - k
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>Polynomial.derivative ↑n = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Polynomial.derivative (OfNat.ofNat n) = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>x : ℕ<VAR>hx : p.natDegree < x<GOAL>(⇑Polynomial.derivative)^[x] p = 0
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>k : ℕ<VAR>h : 0 < k<GOAL>(⇑Polynomial.derivative)^[k] (Polynomial.C a) = 0
<VAR>R : Type u<VAR>Semiring R<VAR>k : ℕ<VAR>h : 0 < k<GOAL>(⇑Polynomial.derivative)^[k] 1 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>k : ℕ<VAR>h : 1 < k<GOAL>(⇑Polynomial.derivative)^[k] Polynomial.X = 0
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : Polynomial.derivative f = 0<GOAL>f.natDegree = 0
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : Polynomial.derivative f = 0<GOAL>f = Polynomial.C (f.coeff 0)
<VAR>R : Type u<VAR>Semiring R<VAR>f g : R[X]<GOAL>Polynomial.derivative (f * g) = Polynomial.derivative f * g + f * Polynomial.derivative g
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>x : R<GOAL>Polynomial.eval x (Polynomial.derivative p) = p.sum fun n a => a * ↑n * x ^ (n - 1)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>p : R[X]<VAR>f : R →+* S<GOAL>Polynomial.derivative (Polynomial.map f p) = Polynomial.map f (Polynomial.derivative p)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>k : ℕ<GOAL>(⇑Polynomial.derivative)^[k] (Polynomial.map f p) = Polynomial.map f ((⇑Polynomial.derivative)^[k] p)
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>f : R[X]<GOAL>Polynomial.derivative (↑n * f) = ↑n * Polynomial.derivative f
<VAR>R : Type u<VAR>Semiring R<VAR>n k : ℕ<VAR>f : R[X]<GOAL>(⇑Polynomial.derivative)^[k] (↑n * f) = ↑n * (⇑Polynomial.derivative)^[k] f
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroSMulDivisors ℕ R<VAR>p : R[X]<VAR>n : ℕ<GOAL>n ∈ (Polynomial.derivative p).support ↔ n + 1 ∈ p.support
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroSMulDivisors ℕ R<VAR>p : R[X]<VAR>hp : 0 < p.natDegree<GOAL>(Polynomial.derivative p).degree = ↑(p.natDegree - 1)
<VAR>R : Type u<VAR>Semiring R<VAR>k : ℕ<VAR>p : R[X]<VAR>m : ℕ<GOAL>((⇑Polynomial.derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>p q : R[X]<GOAL>(⇑Polynomial.derivative)^[n] (p * q) = ∑ k ∈ Finset.range n.succ, n.choose k • ((⇑Polynomial.derivative)^[n - k] p * (⇑Polynomial.derivative)^[k] q)
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>Polynomial.derivative (p ^ (n + 1)) = Polynomial.C (↑n + 1) * p ^ n * Polynomial.derivative p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>Polynomial.derivative (p ^ n) = Polynomial.C ↑n * p ^ (n - 1) * Polynomial.derivative p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<GOAL>Polynomial.derivative (p ^ 2) = Polynomial.C 2 * p * Polynomial.derivative p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>dvd : q ^ n ∣ p<GOAL>q ^ (n - 1) ∣ Polynomial.derivative p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>m : ℕ<VAR>dvd : q ^ n ∣ p<GOAL>q ^ (n - m) ∣ (⇑Polynomial.derivative)^[m] p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<VAR>n m : ℕ<GOAL>p ^ (n - m) ∣ (⇑Polynomial.derivative)^[m] (p ^ n)
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : R[X]<VAR>n : ℕ<VAR>m : ℕ<VAR>c : R<VAR>hm : m ≠ 0<GOAL>↑n ∣ Polynomial.eval c ((⇑Polynomial.derivative)^[m] (f ^ n))
<VAR>R : Type u<VAR>CommSemiring R<VAR>n k : ℕ<GOAL>(⇑Polynomial.derivative)^[k] (Polynomial.X ^ n) = ↑(n.descFactorial k) * Polynomial.X ^ (n - k)
<VAR>R : Type u<VAR>CommSemiring R<VAR>n k : ℕ<GOAL>(⇑Polynomial.derivative)^[k] (Polynomial.X ^ n) = Polynomial.C ↑(n.descFactorial k) * Polynomial.X ^ (n - k)
<VAR>R : Type u<VAR>CommSemiring R<VAR>n k : ℕ<GOAL>(⇑Polynomial.derivative)^[k] (Polynomial.X ^ n) = ↑(n.descFactorial k) • Polynomial.X ^ (n - k)
<VAR>R : Type u<VAR>CommSemiring R<VAR>c : R<VAR>m : ℕ<GOAL>Polynomial.derivative ((Polynomial.X + Polynomial.C c) ^ m) = Polynomial.C ↑m * (Polynomial.X + Polynomial.C c) ^ (m - 1)
<VAR>R : Type u<VAR>CommSemiring R<VAR>c : R<GOAL>Polynomial.derivative ((Polynomial.X + Polynomial.C c) ^ 2) = Polynomial.C 2 * (Polynomial.X + Polynomial.C c)
<VAR>R : Type u<VAR>CommSemiring R<VAR>n k : ℕ<VAR>c : R<GOAL>(⇑Polynomial.derivative)^[k] ((Polynomial.X + Polynomial.C c) ^ n) = n.descFactorial k • (Polynomial.X + Polynomial.C c) ^ (n - k)
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<GOAL>Polynomial.derivative (p.comp q) = Polynomial.derivative q * (Polynomial.derivative p).comp q
<VAR>R : Type u<VAR>CommSemiring R<VAR>p q : R[X]<GOAL>Polynomial.derivative (Polynomial.eval₂ Polynomial.C q p) = Polynomial.eval₂ Polynomial.C q (Polynomial.derivative p) * Polynomial.derivative q
<VAR>R : Type u<VAR>ι : Type y<VAR>CommSemiring R<VAR>DecidableEq ι<VAR>s : Multiset ι<VAR>f : ι → R[X]<GOAL>Polynomial.derivative (Multiset.map f s).prod = (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * Polynomial.derivative (f i)) s).sum
<VAR>R : Type u<VAR>Ring R<VAR>f : R[X]<GOAL>Polynomial.derivative (-f) = -Polynomial.derivative f
<VAR>R : Type u<VAR>Ring R<VAR>f : R[X]<VAR>k : ℕ<GOAL>(⇑Polynomial.derivative)^[k] (-f) = -(⇑Polynomial.derivative)^[k] f
<VAR>R : Type u<VAR>Ring R<VAR>f g : R[X]<GOAL>Polynomial.derivative (f - g) = Polynomial.derivative f - Polynomial.derivative g
<VAR>R : Type u<VAR>Ring R<VAR>c : R<GOAL>Polynomial.derivative (Polynomial.X - Polynomial.C c) = 1
<VAR>R : Type u<VAR>Ring R<VAR>k : ℕ<VAR>f g : R[X]<GOAL>(⇑Polynomial.derivative)^[k] (f - g) = (⇑Polynomial.derivative)^[k] f - (⇑Polynomial.derivative)^[k] g
<VAR>R : Type u<VAR>Ring R<VAR>n : ℤ<GOAL>Polynomial.derivative ↑n = 0
<VAR>R : Type u<VAR>Ring R<VAR>n : ℤ<VAR>f : R[X]<GOAL>Polynomial.derivative (↑n * f) = ↑n * Polynomial.derivative f
<VAR>R : Type u<VAR>Ring R<VAR>n : ℤ<VAR>k : ℕ<VAR>f : R[X]<GOAL>(⇑Polynomial.derivative)^[k] (↑n * f) = ↑n * (⇑Polynomial.derivative)^[k] f
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<GOAL>Polynomial.derivative (p.comp (1 - Polynomial.X)) = -(Polynomial.derivative p).comp (1 - Polynomial.X)
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>k : ℕ<GOAL>(⇑Polynomial.derivative)^[k] (p.comp (1 - Polynomial.X)) = (-1) ^ k * ((⇑Polynomial.derivative)^[k] p).comp (1 - Polynomial.X)
<VAR>R : Type u<VAR>CommRing R<VAR>DecidableEq R<VAR>S : Multiset R<VAR>r : R<VAR>hr : r ∈ S<GOAL>Polynomial.eval r (Polynomial.derivative (Multiset.map (fun a => Polynomial.X - Polynomial.C a) S).prod) = (Multiset.map (fun a => r - a) (S.erase r)).prod
<VAR>R : Type u<VAR>CommRing R<VAR>c : R<VAR>m : ℕ<GOAL>Polynomial.derivative ((Polynomial.X - Polynomial.C c) ^ m) = Polynomial.C ↑m * (Polynomial.X - Polynomial.C c) ^ (m - 1)
<VAR>R : Type u<VAR>CommRing R<VAR>c : R<GOAL>Polynomial.derivative ((Polynomial.X - Polynomial.C c) ^ 2) = Polynomial.C 2 * (Polynomial.X - Polynomial.C c)
<VAR>R : Type u<VAR>CommRing R<VAR>n k : ℕ<VAR>c : R<GOAL>(⇑Polynomial.derivative)^[k] ((Polynomial.X - Polynomial.C c) ^ n) = n.descFactorial k • (Polynomial.X - Polynomial.C c) ^ (n - k)
<VAR>R : Type u<VAR>CommRing R<VAR>n : ℕ<VAR>c : R<GOAL>(⇑Polynomial.derivative)^[n] ((Polynomial.X - Polynomial.C c) ^ n) = ↑n.factorial
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>Ring A<VAR>Algebra R A<VAR>CharZero A<GOAL>{x | IsAlgebraic R x}.Infinite
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>Ring A<VAR>Algebra R A<VAR>CharZero A<GOAL>ℵ₀ ≤ #{ x // IsAlgebraic R x }
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>CommRing A<VAR>IsDomain A<VAR>Algebra R A<VAR>NoZeroSMulDivisors R A<GOAL>Cardinal.lift.{u, v} #{ x // IsAlgebraic R x } ≤ Cardinal.lift.{v, u} #R[X] * ℵ₀
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>CommRing A<VAR>IsDomain A<VAR>Algebra R A<VAR>NoZeroSMulDivisors R A<GOAL>Cardinal.lift.{u, v} #{ x // IsAlgebraic R x } ≤ max (Cardinal.lift.{v, u} #R) ℵ₀
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>CommRing A<VAR>IsDomain A<VAR>Algebra R A<VAR>NoZeroSMulDivisors R A<VAR>Infinite R<GOAL>Cardinal.lift.{u, v} #{ x // IsAlgebraic R x } = Cardinal.lift.{v, u} #R
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>CommRing A<VAR>IsDomain A<VAR>Algebra R A<VAR>NoZeroSMulDivisors R A<VAR>Countable R<GOAL>{x | IsAlgebraic R x}.Countable
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>CommRing A<VAR>IsDomain A<VAR>Algebra R A<VAR>NoZeroSMulDivisors R A<VAR>Countable R<VAR>CharZero A<VAR>IsDomain R<GOAL>#{ x // IsAlgebraic R x } = ℵ₀
<VAR>R A : Type u<VAR>CommRing R<VAR>CommRing A<VAR>IsDomain A<VAR>Algebra R A<VAR>NoZeroSMulDivisors R A<GOAL>#{ x // IsAlgebraic R x } ≤ #R[X] * ℵ₀
<VAR>R A : Type u<VAR>CommRing R<VAR>CommRing A<VAR>IsDomain A<VAR>Algebra R A<VAR>NoZeroSMulDivisors R A<GOAL>#{ x // IsAlgebraic R x } ≤ max #R ℵ₀
<VAR>R A : Type u<VAR>CommRing R<VAR>CommRing A<VAR>IsDomain A<VAR>Algebra R A<VAR>NoZeroSMulDivisors R A<VAR>Infinite R<GOAL>#{ x // IsAlgebraic R x } = #R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>self : CategoryTheory.HalfBraiding X<VAR>U U' : C<GOAL>(self.β (U ⊗ U')).hom = (α_ X U U').inv ≫ (self.β U).hom ▷ U' ≫ (α_ U X U').hom ≫ U ◁ (self.β U').hom ≫ (α_ U U' X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>self : CategoryTheory.HalfBraiding X<VAR>U U' : C<VAR>f : U ⟶ U'<GOAL>X ◁ f ≫ (self.β U').hom = (self.β U).hom ≫ f ▷ X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.Center C<VAR>self : X.Hom Y<VAR>U : C<GOAL>self.f ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ self.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.Center C<VAR>f g : X ⟶ Y<VAR>w : f.f = g.f<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : CategoryTheory.Center C<GOAL>(𝟙 X).f = 𝟙 X.fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : CategoryTheory.Center C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).f = f.f ≫ g.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.Center C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f.f<GOAL>(CategoryTheory.Center.isoMk f).inv.f = CategoryTheory.inv f.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.Center C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f.f<GOAL>(CategoryTheory.Center.isoMk f).hom = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.Center C<GOAL>(X.tensorObj Y).fst = X.fst ⊗ Y.fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.Center C<VAR>U : C<GOAL>(X.tensorObj Y).snd.β U = α_ X.fst Y.fst U ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso X.fst (Y.snd.β U) ≪≫ (α_ X.fst U Y.fst).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (X.snd.β U) Y.fst ≪≫ α_ U X.fst Y.fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : CategoryTheory.Center C<VAR>Y₁ Y₂ : CategoryTheory.Center C<VAR>f : Y₁ ⟶ Y₂<VAR>U : C<GOAL>(X.fst ◁ f.f) ▷ U ≫ ((X.tensorObj Y₂).snd.β U).hom = ((X.tensorObj Y₁).snd.β U).hom ≫ U ◁ X.fst ◁ f.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ : CategoryTheory.Center C<VAR>f : X₁ ⟶ X₂<VAR>Y : CategoryTheory.Center C<VAR>U : C<GOAL>f.f ▷ Y.fst ▷ U ≫ ((X₂.tensorObj Y).snd.β U).hom = ((X₁.tensorObj Y).snd.β U).hom ≫ U ◁ f.f ▷ Y.fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ Y₁ X₂ Y₂ : CategoryTheory.Center C<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>(CategoryTheory.Center.tensorHom f g).f = f.f ⊗ g.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>U : C<GOAL>CategoryTheory.Center.tensorUnit.snd.β U = λ_ U ≪≫ (ρ_ U).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>CategoryTheory.Center.tensorUnit.fst = 𝟙_ C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.Center C<GOAL>(X ⊗ Y).fst = X.fst ⊗ Y.fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.Center C<VAR>U : C<GOAL>(X ⊗ Y).snd.β U = α_ X.fst Y.fst U ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso X.fst (Y.snd.β U) ≪≫ (α_ X.fst U Y.fst).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (X.snd.β U) Y.fst ≪≫ α_ U X.fst Y.fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : CategoryTheory.Center C<VAR>Y₁ Y₂ : CategoryTheory.Center C<VAR>f : Y₁ ⟶ Y₂<GOAL>(X ◁ f).f = X.fst ◁ f.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ : CategoryTheory.Center C<VAR>f : X₁ ⟶ X₂<VAR>Y : CategoryTheory.Center C<GOAL>(f ▷ Y).f = f.f ▷ Y.fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ Y₁ X₂ Y₂ : CategoryTheory.Center C<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>(f ⊗ g).f = f.f ⊗ g.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>U : C<GOAL>(𝟙_ (CategoryTheory.Center C)).snd.β U = λ_ U ≪≫ (ρ_ U).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : CategoryTheory.Center C<GOAL>(α_ X Y Z).hom.f = (α_ X.fst Y.fst Z.fst).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : CategoryTheory.Center C<GOAL>(α_ X Y Z).inv.f = (α_ X.fst Y.fst Z.fst).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : CategoryTheory.Center C<GOAL>(λ_ X).hom.f = (λ_ X.fst).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : CategoryTheory.Center C<GOAL>(λ_ X).inv.f = (λ_ X.fst).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : CategoryTheory.Center C<GOAL>(ρ_ X).hom.f = (ρ_ X.fst).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : CategoryTheory.Center C<GOAL>(ρ_ X).inv.f = (ρ_ X.fst).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.Center.forget C).ε = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>∀ {X Y : CategoryTheory.Center C} (f : X ⟶ Y), (CategoryTheory.Center.forget C).map f = f.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.Center C<GOAL>(CategoryTheory.Center.forget C).μ X Y = 𝟙 (X.fst ⊗ Y.fst)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : CategoryTheory.Center C<GOAL>(CategoryTheory.Center.forget C).obj X = X.fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.Center C<GOAL>(X.braiding Y).hom.f = (X.snd.β Y.fst).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.Center C<GOAL>(X.braiding Y).inv.f = (X.snd.β Y.fst).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(CategoryTheory.Center.ofBraidedObj X).fst = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<GOAL>(CategoryTheory.Center.ofBraidedObj X).snd.β Y = β_ X Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<GOAL>((CategoryTheory.Center.ofBraided C).μ X Y).f = 𝟙 ({ obj := CategoryTheory.Center.ofBraidedObj, map := fun {X Y} f => { f := f, comm := ⋯ }, map_id := ⋯, map_comp := ⋯ }.obj X ⊗ { obj := CategoryTheory.Center.ofBraidedObj, map := fun {X Y} f => { f := f, comm := ⋯ }, map_id := ⋯, map_comp := ⋯ }.obj Y).fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CategoryTheory.Center.ofBraided C).ε.f = 𝟙 (𝟙_ (CategoryTheory.Center C)).fst