Define "log using an arbitrary base" function and then prove some of its properties. This builds on previous work by Stefan O'Rear.
This supports the notational form ; that looks a little more like traditional notation, but is different from other 2-parameter functions. E.g., .
This form is less convenient to work with inside set.mm as compared to the form defined separately.