diff --git a/algebra/field.math b/algebra/field.math index 60c9171..81d61df 100644 --- 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 index e5444c8..9fa3876 100644 --- 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'