diff options
| author | Cyril Cohen | 2020-05-29 17:42:29 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-06-06 01:43:35 +0200 |
| commit | 04e78bbeefe509bd8b84cb222a1322774ce03aec (patch) | |
| tree | a4175a4e5b8cab538ebd8ad82dd35109de23d790 /mathcomp/field | |
| parent | 43459547cbcd9d7987a083829171a589ba98bf81 (diff) | |
Generalizing max and min to porderType
- max and min are not defined in terms or meet and join anymore
- extremum_inP is a generalization of extremum suitable for a partial order
- arg_min and arg_max are usable in a porderType
- equivalences between min and meet, and max and join are proven for orderType
- leP, ltP, ltgtP, and `[l]?comparable_.*P` lemmas have been generalized to take this into account
- total_display was completely removed
Diffstat (limited to 'mathcomp/field')
0 files changed, 0 insertions, 0 deletions