[Merged by Bors] - feat(topology/algebra/order): ⁻¹ continuous for linear ordered fields

[ericrbg]

Closes #12781.

---

[ericrbg]

should we also make the topological_division_ring instance with this or is there TC loops with that? where would we put it?

[YaelDillies]

If this is also true for linear ordered semifields, then we will be able to get rid of nnreal.has_continuous_inv₀

[ericrbg]

Oh, it should be from my memory. I'll try do that generalisation tomorrow.

[eric-wieser]

We don't have a typeclass for linearly ordered semifields though, do we?

[ericrbg]

No, we don't. And I just remembered I used a lot of subtraction (3am brain isn't great) - I think it can be worked around, but not 100% sure.

[eric-wieser]

Maybe it's worth just leaving a TODO comment summarizing Yael's point (or asking @YaelDillies to suggest one themself); actually addressing it seems out of scope here.

[eric-wieser]

should we also make the topological_division_ring instance with this or is there TC loops with that? where would we put it?

I think you'd be safe from typeclass loops, there aren't many instances of topological_division_ring.

[ericrbg]

done; I'm curious how my structure building works there, I don't provide the topological_ring instance.

[YaelDillies]

#15027 for linear_ordered_semifield. Maybe we will also need topological_division_semiring? My point about nnreal.has_continuous_inv₀ is that in theory you should be able to copy-paste its proof.

[ericrbg]

the proof seems to be based on the real coercion

[ericrbg]

Thanks, that works! How come I don't need to provide the topological_ring instance as well, and TC just picks it up?

[eric-wieser]

I think that's because it's a new-style structure.

[ocfnash]

I think it's worth adding a comment about generalising to the non-existent topological_division_semiring with application to nnreal but otherwise this LGTM.

bors d+

[bors]

✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ericrbg]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests