diff options
| author | Pierre-Yves Strub | 2020-01-30 10:54:10 +0100 |
|---|---|---|
| committer | GitHub | 2020-01-30 10:54:10 +0100 |
| commit | 7d04173b52cf02717b8f8e8c13bb7c3521de7e89 (patch) | |
| tree | 1d350743e8bf7a8fbebcfba6cbdba447750768ee /mathcomp/field | |
| parent | d3f5e11aa1bbdf6ee4a111bf4641d162d289340f (diff) | |
| parent | 2d98f0cd2a5f69d2b3da77b738376cc812510ec7 (diff) | |
Merge pull request #453 from pi8027/experiment/order-nondistr-lattice
Non-distributive lattice structures
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. |