***********************
Note 4:15 start time!
***********************

Floor division (also called integer division or Euclidean division) is the operation that divides two integers and discards the remainder. Floor division satisfies some nontrivial identities, such as this one proposed by Ramanujan in 1918:

\[ \lfloor \frac{n}{3} \rfloor + \lfloor \frac{n+2}{6} \rfloor + \lfloor \frac{n+4}{6} \rfloor = \lfloor \frac{n}{2} \rfloor + \lfloor \frac{n+3}{6} \rfloor. \]

How can we systematically verify such an equation (without resorting to case bashing)? And can we characterize the set of all such equations in a perspicuous way? To answer these questions, I present a sound and complete axiomatization for the equational theory of linear arithmetic with operations for floor division by fixed positive integers. My axiomatization has five axiom schemata. Three of these are somewhat obvious, but the remaining two are more interesting. One is a variant of Hermite's identity, discovered in 1884. The other appears to be a hitherto unnoticed identity, which is perhaps surprising for an identity involving only elementary operations. I prove that my axiomatization is complete by showing that the axioms suffice to put every term into a normal form, and this normal form may be of independent interest. My hope is that, by the end of this talk, you will have the tools to develop a greater dexterity in manipulating expressions involving floor division, so that you can readily see the truth of identities like the one above.