Left and right multiplication sets

Provides leftMul a = Ra, rightMul a = aR, the leftIdealOfElement constructor, and the consequence that aRb = 0 collapses these auxiliary sets to zero. Used by the prime ring characterisation.

def LeanPool.ArtinWedderburn.leftMul {R : Type u_1} [Ring R] (a : R) : Set R

The set Ra = {r * a | r : R} of left multiples of a.

Equations

• LeanPool.ArtinWedderburn.leftMul a = {x : R | ∃ (r : R), x = r * a}

def LeanPool.ArtinWedderburn.rightMul {R : Type u_1} [Ring R] (a : R) : Set R

The set aR = {a * r | r : R} of right multiples of a.

Equations

• LeanPool.ArtinWedderburn.rightMul a = {x : R | ∃ (r : R), x = a * r}

theorem LeanPool.ArtinWedderburn.left_mul_zero_impl_mul_zero {R : Type u_1} [Ring R] (a b : R) : bothMul a b = {0} → a * b = 0

theorem LeanPool.ArtinWedderburn.in_particular {R : Type u_1} [Ring R] (a c b : R) : bothMul a b = {0} → a * c * b = 0

theorem LeanPool.ArtinWedderburn.both_mul_zero_one_left_zero {R : Type u_1} [Ring R] (a b : R) : bothMul a b = {0} → leftMul a * leftMul b = {0}

def LeanPool.ArtinWedderburn.leftIdealOfElement {R : Type u_1} [Ring R] (a : R) : Ideal R

The principal left ideal Ra generated by a, packaged as an Ideal R.

Equations

• LeanPool.ArtinWedderburn.leftIdealOfElement a = { carrier := LeanPool.ArtinWedderburn.leftMul a, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem LeanPool.ArtinWedderburn.carrier_of_left_ideal_of_element {R : Type u_1} [Ring R] (a : R) : (leftIdealOfElement a).carrier = leftMul a