Division subrings and division rings

Defines IsDivisionSubring and IsDivisionRing, supplies the conversion to Mathlib's DivisionRing, and shows that an isomorphism of rings transports the division-ring property.

def LeanPool.ArtinWedderburn.IsDivisionSubring {R : Type u_1} [Ring R] (S : NonUnitalSubring R) (e : R) : Prop

S is a division subring with identity e when it contains a nonzero element and every nonzero member has a left inverse inside S equal to e.

Equations

• LeanPool.ArtinWedderburn.IsDivisionSubring S e = ((∃ x ∈ S, x ≠ 0) ∧ ∀ x ∈ S, x ≠ 0 → ∃ y ∈ S, y * x = e)

def LeanPool.ArtinWedderburn.IsDivisionRing (R : Type u_2) [Ring R] : Prop

A ring R is a division ring when it is nontrivial and every nonzero element has a two-sided multiplicative inverse.

Equations

• LeanPool.ArtinWedderburn.IsDivisionRing R = ((∃ (x : R), x ≠ 0) ∧ ∀ (x : R), x ≠ 0 → ∃ (y : R), y * x = 1 ∧ x * y = 1)

theorem LeanPool.ArtinWedderburn.left_inv_implies_divring {R : Type u_1} [Ring R] [Nontrivial R] (h : ∀ (x : R), x ≠ 0 → ∃ (y : R), y * x = 1) : IsDivisionRing R

@[reducible]

noncomputable def LeanPool.ArtinWedderburn.IsDivisionRingToDivisionRing {R : Type u_1} [Ring R] (div : IsDivisionRing R) : DivisionRing R

Promote a proof of IsDivisionRing R to a Mathlib DivisionRing R instance.

Equations

• LeanPool.ArtinWedderburn.IsDivisionRingToDivisionRing div = DivisionRing.ofIsUnitOrEqZero ⋯

theorem LeanPool.ArtinWedderburn.isomorphic_ring_div {R : Type u_1} [Ring R] {R' : Type u_2} [Ring R'] (f : R ≃+* R') (h_div : IsDivisionRing R) : IsDivisionRing R'