Add the ad4ant* and ad5ant* ones to iset.mm too if you have the time (if
not, no worries, it can happen whenever someone gets around to it).
The supadd and inisegn0 ones wouldn't work in iset.mm.
On 8/15/20 6:17 AM, Glauco wrote:
I've taken advantage of some theorems, still in mathboxes. Can I
You have my approval.
Norm
On Saturday, August 15, 2020 at 9:17:56 AM UTC-4, Glauco wrote:
>
> I've taken advantage of some theorems, still in mathboxes. Can I set up a
> PR for moving them to the main body?
>
> Here's the list:
>
> - supadd from Brendan Leahy's mathbox : sup distributes over
I've taken advantage of some theorems, still in mathboxes. Can I set up a
PR for moving them to the main body?
Here's the list:
- supadd from Brendan Leahy's mathbox : sup distributes over addition (we
already have supmul in the main part, that's "the same" for multiplication)
- inisegn0 from
