diff options
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index b41d5ec..0a759e8 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -586,13 +586,8 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. by rewrite v_gt0 /= -if_neg posNneg. by rewrite v_lt0 /= -if_neg -(opprK v) posN posNneg ?posN. have absE v: le 0 v -> abs v = v by rewrite /abs => ->. - pose QyNum : realLtMixin (Q y) := - RealLtMixin posD posM posNneg posB posVneg absN absE (rrefl _). - pose QyOrder := - OrderType - (DistrLatticeType (POrderType ring_display (Q y) QyNum) QyNum) QyNum. - pose QyNumField := [numFieldType of NumDomainType QyOrder QyNum]. - pose Ry := [realFieldType of [realDomainType of QyNumField]]. + pose Ry := LtRealFieldOfField + (RealLtMixin posD posM posNneg posB posVneg absN absE (rrefl _)). have archiRy := @rat_algebraic_archimedean Ry _ alg_integral. by exists (ArchiFieldType Ry archiRy); apply: [rmorphism of idfun]. have some_realC: realC. |