Equations.lean vs Chapter 2

Stream: Equational

[Andrés Goens]

The equations in Chapter 2 don't seem to correspond to Equations.lean. I had an error in CI in equational#460 because equation 953 is used in Subgraph.lean and is refered to in Chapter 2, but was not in Equations.lean (it was transitively being imported through the backdoor, accidentally I presume). There are more though, like 477, that's also in Chapter 2 but not in Equations.lean. Should these two agree? Should we add the missing ones from the blueprint to the file, or vice-versa?

[Terence Tao]

I think Equations.lean is a cleaner source of "ground truth" for equations of interest than the blueprint, but I agree that it is worth aligning them. I can take a shot at that later today.