diff options
| author | Kazuhiko Sakaguchi | 2019-10-30 14:40:23 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-12-11 14:26:52 +0100 |
| commit | 44e8df83ad4e4394a96c15c787405cdea8931074 (patch) | |
| tree | 20d4068c0d84639e7c2237b063c385d9f86c110f /mathcomp/field | |
| parent | d913820cc104a43117604469dc47fca7114a98bd (diff) | |
Rename: (l|L)attice -> (d|D)istrLattice
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. |