diff options
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 4fe5f70..4824697 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -589,7 +589,8 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. pose QyNum : realLtMixin (Q y) := RealLtMixin posD posM posNneg posB posVneg absN absE (rrefl _). pose QyOrder := - OrderType (LatticeType (POrderType ring_display (Q y) QyNum) QyNum) QyNum. + OrderType + (DistrLatticeType (POrderType ring_display (Q y) QyNum) QyNum) QyNum. pose QyNumField := [numFieldType of NumDomainType QyOrder QyNum]. pose Ry := [realFieldType of [realDomainType of QyNumField]]. have archiRy := @rat_algebraic_archimedean Ry _ alg_integral. |