use ring and ring with identity instead of rng and ring

mathlingua · Aug 11, 2023 · a63c614 · a63c614
1 parent a4106eb
commit a63c614
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 44 deletions.
diff --git a/algebra/field.math b/algebra/field.math
@@ -3,18 +3,8 @@
 ::
 
 [\field]
-Defines: F := (X, +, *, 0, 1)
-means: 'F is \commutative.ring & \nontrivial.ring'
-specifies:
-. forAll: x
-  where: 'x [in]: X'
-  suchThat: 'x != 0'
-  then:
-  . exists: y
-    where: 'y [in]: F'
-    suchThat:
-    . 'x * y = 1'
-    . 'y * x = 1'
+Defines: F
+means: 'F is \commutative.ring.with.identity & \division.ring'
 Provides:
 . symbol: 'x [in]: F :-> x is \field.element:of{F}'
 Documented:

diff --git a/algebra/ring.math b/algebra/ring.math
@@ -2,41 +2,11 @@
 # Rings
 ::
 
-[\rng]
-Describes: R := (X, +, *, 0)
-extends:
-. '(X, "+", 0) is \abelian.group'
-. '(X, "*") is \semigroup'
-satisfies:
-. forAll: x, y, z
-  where: 'x, y, z [in]: R'
-  then:
-  . 'x * (y + z) = (x * y) + (x * z)'
-  . '(x + y) * z = (x * z) + (y * z)'
-Provides:
-. 'x [in]: R :-> x is \rng.element:of{G}'
-Documented:
-. called: "rng"
-------------------------------------------
-Id: "f3807860-4fda-44fd-ba39-bee2c224f045"
-
-
-[\rng.element:of{R}]
-Describes: x
-when: 'R is \rng'
-extends:
-. 'x is \group.element:of{R}'
-. 'x is \semigroup.element:of{R}'
-Documented:
-. called: "rng element of R?"
-------------------------------------------
-Id: "79a0237f-b678-4d6a-ba1f-aadc40283828"
-
 
 [\ring]
 Describes: R := (X, +, *, 0)
 extends:
-. 'R is \rng'
+. '(X, "+", 0) is \abelian.group'
 . '(X, "*") is \semigroup'
 satisfies:
 . [distributive.law]
@@ -57,7 +27,7 @@ Id: "bd519191-1c37-426d-8fda-e5855407e6cd"
 Describes: x
 when: 'R is \ring'
 extends:
-. 'x is \rng.element:of{R}'
+. 'x is \group.element:of{R}'
 . 'x is \semigroup.element:of{R}'
 Documented:
 . called: "ring element of R?"
@@ -101,6 +71,15 @@ Documented:
 Id: "3352fddf-6cce-4a0d-93b7-9f79c493f942"
 
 
+[\commutative.ring.with.identity]
+Describes: R
+extends: 'R is \ring.with.identity & \commutative.ring'
+Documented:
+. called: "commutative ring with identity"
+------------------------------------------
+Id: "57d40c75-7b95-4680-ac65-414efa306beb"
+
+
 [\trivial.ring]
 Defines: R := (X, +, *, 0)
 means: 'R is \ring'