diff --git a/BinomialNotes.txt b/BinomialNotes.txt
index 9431bce..1e50e5c 100644
--- a/BinomialNotes.txt
+++ b/BinomialNotes.txt
@@ -1,6 +1,7 @@
 Part I, Goal:
 
 Introduce binomial rings, following J. Elliot's paper.
+
 Binomial rings are torsion-free commutative rings R such that for any x ∈ R and any k ∈ ℕ, we have k! | x(x-1)⋯(x-k+1).
 The torsion-free condition implies multiplication by k! is injective, so we define `choose x k` to be the unique y such that y*k! = x(x-1)⋯(x-k+1).
 
@@ -10,13 +11,13 @@ We define multichoose x k to be the unique function satisfying k! | x(x+1)⋯(x+
 
 Part II, Theorems about binomial coefficients we need for vertex algebras:
 
-0. Z is a binomial ring (done).  If ℚ ⊂ R, then k! is invertible, so R is binomial (not done).
-1. When x ∈ ℕ, Ring.choose agrees with nat.choose (done)
+0. Z is a binomial ring.  If ℚ ⊂ R, then k! is invertible, so R is binomial.
+1. When x ∈ ℕ, Ring.choose agrees with nat.choose.
 2. nat.choose_mul : n.choose k * k.choose s = n.choose s * (n-s).choose (k-s) when k \geq s
    An alternative form is x.choose (n+k) * (n+k).choose k = x.choose n * (x-n).choose k
    so we know which terms need to be non-negative.
 3. (-1)^k x.choose k = (k-x-1).choose k
-4. Vandermonde convolution: (x+y).choose k = (finset.range (k+1)).sum (λ (i:ℕ), x.choose i * y.choose (k-i))
+4. Vandermonde convolution: (x+y).choose k = \sum ij \in antidiagonal k, x.choose ij.1 * y.choose ij.2
 
 Theorems about series we need:
 1. Expansions of (x-y)^(-N) when |x| < |y| and |y| < |x| - A good treatment of Hahn series in two variables should make this work.
@@ -27,15 +28,15 @@ Theorems about series we need:
 
 Part III, Implementation plan:
 
-All theorems are finished.
+All theorems are finished and merged into Mathlib4.
 
 Part IV, To do:
 
-Consider proving some of Elliott's other results (#7 is in fact relevant):
+Consider proving some of Elliott's other results (#7 may be relevant):
 1. The integer-valued polynomial rings (generated by Ring.choose x_i n) are free (commutative) binomial rings.  That is, we get a left adjoint to the forgetful functor to sets.
 2. A commutative ring is binomial if and only if it is a \lambda-ring whose Adams operations are all identity.
 3. There is a right-adjoint to the forgetful functor from commutative binomial rings to commutative rings, and the universal \lambda ring is a module.
-4. There is a right-adjoint to the inclusion of binomial rings to \lambda-ringsm namely the functor that takes a \lambda-ring to the largest subring on which Adams operations are identity.
+4. There is a right-adjoint to the inclusion of binomial rings to \lambda-rings, namely the functor that takes a \lambda-ring to the largest subring on which Adams operations are identity.
 4. A presentation of the ring of integer-valued polynomials.
 5. In order that a commutative ring A be binomial, it is necessary and sufficient that for all primes p and a \in A, a^p \equiv a mod pA.
 6. Smallest enveloping binomial ring of a torsion-free ring.