PR #3292: feat(field_theory/complete_ordered): conditiona...

Stream: triage

[Random Issue Bot]

Today I chose PR 3292 for discussion!

feat(field_theory/complete_ordered): conditionally_complete_linear_ordered_field, aka the reals
Created by @Alex J Best (@alexjbest) on 2020-07-05
Labels: needs-documentation

Is this PR still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

All prerequisites are in mathlib now, so we just need a big cleanup.