blob: 657fa8f87caf03de66740dea2937df4400260571 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Algebraic properties of ordered commutative rings
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
open import Helium.Algebra.Ordered.StrictTotal.Bundles
module Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing
{ℓ₁ ℓ₂ ℓ₃}
(commutativeRing : CommutativeRing ℓ₁ ℓ₂ ℓ₃)
where
open CommutativeRing commutativeRing
renaming
( trans to <-trans
; irrefl to <-irrefl
; asym to <-asym
; 0<a+0<b⇒0<ab to x>0∧y>0⇒x*y>0
)
open import Algebra.Properties.Ring Unordered.ring public
renaming (-0#≈0# to -0≈0)
open import Algebra.Properties.Semiring.Mult.TCOptimised Unordered.semiring public
open import Algebra.Properties.CommutativeSemiring.Exp.TCOptimised Unordered.commutativeSemiring public
open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
using
( +-mono-<; +-monoˡ-<; +-monoʳ-<
; +-mono-≤; +-monoˡ-≤; +-monoʳ-≤
; +-cancel-<; +-cancelˡ-<; +-cancelʳ-<
; +-cancel-≤; +-cancelˡ-≤; +-cancelʳ-≤
; x≥0∧y>0⇒x+y>0 ; x>0∧y≥0⇒x+y>0
; x≤0∧y<0⇒x+y<0 ; x<0∧y≤0⇒x+y<0
; x≥0∧y≥0⇒x+y≥0 ; x≤0∧y≤0⇒x+y≤0
; x≤0∧x+y>0⇒y>0 ; x≤0∧y+x>0⇒y>0 ; x<0∧x+y≥0⇒y>0 ; x<0∧y+x≥0⇒y>0
; x≥0∧x+y<0⇒y<0 ; x≥0∧y+x<0⇒y<0 ; x>0∧x+y≤0⇒y<0 ; x>0∧y+x≤0⇒y<0
; x≤0∧x+y≥0⇒y≥0 ; x≤0∧y+x≥0⇒y≥0
; x≥0∧x+y≤0⇒y≤0 ; x≥0∧y+x≤0⇒y≤0
; ×-zeroˡ; ×-zeroʳ
; ×-identityˡ
; n≢0⇒×-monoˡ-< ; x>0⇒×-monoʳ-< ; x<0⇒×-anti-monoʳ-<
; ×-monoˡ-≤; x≥0⇒×-monoʳ-≤; x≤0⇒×-anti-monoʳ-≤
; ×-cancelˡ-<; x≥0⇒×-cancelʳ-<; x≤0⇒×-anti-cancelʳ-<
; n≢0⇒×-cancelˡ-≤ ; x>0⇒×-cancelʳ-≤ ; x<0⇒×-anti-cancelʳ-≤
; n≢0∧x>0⇒n×x>0; n≢0∧x<0⇒n×x<0
; x≥0⇒n×x≥0; x≤0⇒n×x≤0
; n×x>0⇒x>0; n×x<0⇒x<0
; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0
; -‿anti-mono-<; -‿anti-mono-≤
; -‿anti-cancel-<; -‿anti-cancel-≤
; x≈0⇒-x≈0 ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
; -x≈0⇒x≈0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
; x<y⇒0<y-x; 0<y-x⇒x<y
; x≤y⇒0≤y-x; 0≤y-x⇒x≤y
; 0≤1; 1≈0⇒x≈y; x≉y⇒0<1; x<y⇒0<1
; x>0⇒*-monoˡ-<; x>0⇒*-monoʳ-<; x<0⇒*-anti-monoˡ-<; x<0⇒*-anti-monoʳ-<
; x≥0⇒*-monoˡ-≤; x≥0⇒*-monoʳ-≤; x≤0⇒*-anti-monoˡ-≤; x≤0⇒*-anti-monoʳ-≤
; x≥0⇒*-cancelˡ-<; x≥0⇒*-cancelʳ-<; x≤0⇒*-anti-cancelˡ-<; x≤0⇒*-anti-cancelʳ-<
; x>0⇒*-cancelˡ-≤; x>0⇒*-cancelʳ-≤; x<0⇒*-anti-cancelˡ-≤; x<0⇒*-anti-cancelʳ-≤
; x≈0⇒x*y≈0; x≈0⇒y*x≈0
; -x*-y≈x*y
; x>0∧y<0⇒x*y<0; x<0∧y>0⇒x*y<0; x<0∧y<0⇒x*y>0
; x≥0∧y≥0⇒x*y≥0; x≥0∧y≤0⇒x*y≤0; x≤0∧y≥0⇒x*y≤0; x≤0∧y≤0⇒x*y≥0
; x>1∧y≥1⇒x*y>1; x≥1∧y>1⇒x*y>1; 0≤x<1∧y≤1⇒x*y<1; x≤1∧0≤y<1⇒x*y<1
; x≥1∧y≥1⇒x*y≥1; 0≤x≤1∧y≤1⇒x*y≤1; x≤1∧0≤y≤1⇒x*y≤1
; x*x≥0; x*y≈0⇒x≈0⊎y≈0
; ^-zeroˡ; ^-zeroʳ
; ^-identityʳ
; n≢0⇒0^n≈0
; x>1⇒^-monoˡ-<; 0<x<1⇒^-anti-monoˡ-<
; x≥1⇒^-monoˡ-≤; 0≤x≤1⇒^-anti-monoˡ-≤
; x>0⇒x^n>0
; x≥0⇒x^n≥0
; x^n≈0⇒x≈0
; x>1∧n≢0⇒x^n>1; 0≤x<1∧n≢0⇒x^n<1
; x≥1⇒x^n≥1; 0≤x≤1⇒x^n≤1
; x<y+z⇒x-z<y
)
|
