Ring Theory

Contents

semiring

A₊C₊0A_·D

Ring

A₊C₊0N₊A_·D

+ : Ring → Ring, · : Ring → Ring, a, b, c, 0 : Ring ⊢ a + (b + c) = (a + b) + c (associative), a + b = b + a (commutative), a + 0 = 0 + a = a (additive identity), a + (-a) = 0 (additive inverse), a (b c) = (a b) c (associative), a (b + c) = a b + a c, (a + b) c = a c + b c (distributive). Z, Q, C ≤ Ring.

a, b : Ring ⊢ a + (-a) = 0 ⇒ -(-a) = a.

Commutative Ring

A₊C₊0N₊A_·C_·D

CommutativeRing ≤ Ring, a, b : CommutativeRing ⊢ a b = b a (commutative).

Ring with Identity

A₊C₊0N₊A_·1D

RingWithIdentity ≤ Ring, a, 1 : RingWithIdentity ⊢ a 1 = 1 a = a.

Integral domain

IntegralDomain ≤ CommutativeRing, a, b, 0 : IntegralDomain ⊢ 1 ≠ 0, a b = 0 ⇒ a = 0 or b = 0. Z, Q ≤ IntegralDomain.

Field

A₊C₊0N₊A_·C_·1N_·D

Field ≤ CommutativeRing × RingWithIdentity, a : Field ⊢ a ≠ 0 ⇒ a^-1 : Field, a a^-1 = 0 (multiplicative inverse). Q, C ≤ Field.

Prime Ideal

Topological Ring

References