Most of these theorems related to restricting a complex function to the reals and taking the derivative. The pull request mostly consists of explaining what would be involved in doing that in iset.mm. It expands a few entries for theorems which already had entries, to explain the differences between set.mm and iset.mm a bit better.
Most of these theorems related to restricting a complex function to the reals and taking the derivative. The pull request mostly consists of explaining what would be involved in doing that in iset.mm. It expands a few entries for theorems which already had entries, to explain the differences between set.mm and iset.mm a bit better.