Jacobson's commutativity theorem

DefinitionPrime two-sided ideal#✓fully proved

A two-sided ideal \(P\) of a ring \(R\) is prime if \(P \ne R\) and, for all \(a, b \in R\), if \(a r b \in P\) for every \(r \in R\), then \(a \in P\) or \(b \in P\).

This is the noncommutative notion of primality; being completely prime (\(P \ne R\), and \(ab \in P\) forces \(a \in P\) or \(b \in P\)) is stronger.

def IsPrimeIdeal (P : TwoSidedIdeal R) : Prop :=
  P ≠ ⊤ ∧ ∀ a b : R, (∀ r : R, a * r * b ∈ P) → a ∈ P ∨ b ∈ P

Used by 1

Used byJacobson's commutativity theorem

Definitionm-system#✓fully proved

A subset \(M\) of a ring \(R\) is an \(m\)-system if it is nonempty, does not contain \(0\), and for all \(a, b \in M\) there is some \(r \in R\) with \(a r b \in M\).

def IsMSystem (M : Set R) : Prop :=
  M.Nonempty ∧ 0 ∉ M ∧ ∀ a b : R, a ∈ M → b ∈ M → ∃ r : R, a * r * b ∈ M

Used by 1

Used byJacobson's commutativity theorem

TheoremJacobson's commutativity theorem#✓fully proved

Let \(R\) be a ring. If for every \(x \in R\) there is a natural number \(n > 1\) with \(x^n = x\), then \(R\) is commutative, that is, \(xy = yx\) for all \(x, y \in R\).

public theorem jacobson_commutativity {R : Type*} [Ring R]
    (h : ∀ x : R, ∃ n : ℕ, 1 < n ∧ x ^ n = x) :
    ∀ x y : R, x * y = y * x

Uses 2

Proof usesm-system · Prime two-sided ideal

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.