diff options
| author | Kazuhiko Sakaguchi | 2019-09-26 22:59:01 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-01-15 20:27:31 +0900 |
| commit | 00f593f9361af73290443fce9b16cc0cbe9884f4 (patch) | |
| tree | 0763d1ab3aa4718741c93124a3c3a4dc0866ee18 /mathcomp/field | |
| parent | 2646a263ba499f50ad09816ef76bea683517da26 (diff) | |
Non-distributive lattice
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. |