mathlib3

632b0312 - feat(algebra/order/complete_field): `conditionally_complete_linear_ordered_field`, aka the reals (#3292)

feat(algebra/order/complete_field): `conditionally_complete_linear_ordered_field`, aka the reals (#3292) Introduce a class `conditionally_complete_linear_ordered_field`, which axiomatises the real numbers. Show that there exist a unique ordered ring isomorphism from any two such. Additionally, show there is a unique order ring hom from any archimedean linear ordered field to such a field, giving that the ordered ring homomorphism from the rationals to the reals is unique for instance. Co-authored-by: Jalex Stark alexmaplegm@gmail.com Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>