Thomas Browning
Thomas Browning
@CBirkbeck You should update the description of the PR to include the new dependencies.
@CBirkbeck Could you merge master?
If you're going to binary search, would it make more sense to just repeatedly double the exponent?
> It turns out there's a "standard trick" for doing this without search: see e.g. section 2.2 of https://arxiv.org/pdf/1007.3615.pdf . I'll investigate whether Sage/Singular supports this trick out of the...
@hrmacbeth Do you have plans to return to this at some point?
> This all feels like it should be much more direct from orbit-stabilizer-like theorems. Maybe @tb65536 has thoughts here? Here's an orbit-stabilizer approach: ``` theorem index_stabilizer (G : Type*) {X...
I'm marking this as awaiting-review in case a lemma other than #12002 would be better for this situation.