Ring Theory
Contents
semiring
A+C+0A·D
Ring
A+C+0N+A·D
+ : Ring → Ring, · : Ring → Ring, a, b, c, 0 : Ring ⊢ a +
a, b : Ring ⊢ 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.