search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
238 stars 87 forks source link

First pass at intuitionizing the rest of the "The natural logarithm on complex numbers" section #4044

Closed jkingdon closed 1 month ago

jkingdon commented 1 month ago

Although some of the functions here (relogcn to logrec) could in principle be intuitionized, none of them seem to be within easy reach.

So this ended up being another set of additions to the missing theorems list in mmil.html.