theorem RingCon.quot_ind {R : Type u_3} [Ring R] (r : RingCon R) {motive : r.Quotient → Prop} (basic : ∀ (x : R), motive (r.mk' x)) (x : r.Quotient) : motive x

theorem TwoSidedIdeal.smul_mem {R : Type u_3} [Ring R] (I : TwoSidedIdeal R) (r : R) {x : R} (hx : x ∈ I) : r • x ∈ I

def TwoSidedIdeal.toMop {R : Type u_3} [Ring R] (rel : TwoSidedIdeal R) : TwoSidedIdeal Rᵐᵒᵖ

Any two-sided-ideal in A corresponds to a two-sided-ideal in Aᵒᵖ.

Equations

• rel.toMop = { ringCon := { r := fun (a b : Rᵐᵒᵖ) => rel.ringCon (MulOpposite.unop b) (MulOpposite.unop a), iseqv := ⋯, mul' := ⋯, add' := ⋯ } }

@[simp]

theorem TwoSidedIdeal.toMop_ringCon_r {R : Type u_3} [Ring R] (rel : TwoSidedIdeal R) (a b : Rᵐᵒᵖ) : rel.toMop.ringCon.toSetoid a b = rel.ringCon (MulOpposite.unop b) (MulOpposite.unop a)

def TwoSidedIdeal.fromMop {R : Type u_3} [Ring R] (rel : TwoSidedIdeal Rᵐᵒᵖ) : TwoSidedIdeal R

Any two-sided-ideal in Aᵒᵖ corresponds to a two-sided-ideal in A.

Equations

• rel.fromMop = { ringCon := { r := fun (a b : R) => rel.ringCon (MulOpposite.op b) (MulOpposite.op a), iseqv := ⋯, mul' := ⋯, add' := ⋯ } }

@[simp]

theorem TwoSidedIdeal.fromMop_ringCon_r {R : Type u_3} [Ring R] (rel : TwoSidedIdeal Rᵐᵒᵖ) (a b : R) : rel.fromMop.ringCon.toSetoid a b = rel.ringCon (MulOpposite.op b) (MulOpposite.op a)

def TwoSidedIdeal.toMopOrderIso {R : Type u_3} [Ring R] : TwoSidedIdeal R ≃o TwoSidedIdeal Rᵐᵒᵖ

Two-sided-ideals of A and that of Aᵒᵖ corresponds bijectively to each other.

Equations

• TwoSidedIdeal.toMopOrderIso = { toFun := TwoSidedIdeal.toMop, invFun := TwoSidedIdeal.fromMop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem TwoSidedIdeal.toMopOrderIso_apply {R : Type u_3} [Ring R] (rel : TwoSidedIdeal R) : toMopOrderIso rel = rel.toMop

@[simp]

theorem TwoSidedIdeal.toMopOrderIso_symm_apply {R : Type u_3} [Ring R] (rel : TwoSidedIdeal Rᵐᵒᵖ) : (RelIso.symm toMopOrderIso) rel = rel.fromMop

theorem TwoSidedIdeal.comap_injective {R : Type u_3} [Ring R] {R' : Type u_4} [Ring R'] {F : Type u_5} [FunLike F R R'] [RingHomClass F R R'] (f : F) (hf : Function.Surjective ⇑f) : Function.Injective fun (J : TwoSidedIdeal R') => comap f J

instance TwoSidedIdeal.instModuleMulOppositeSubtypeMem_brauerGroup {R : Type u_3} [Ring R] (I : TwoSidedIdeal R) : Module Rᵐᵒᵖ ↥I

Equations

• I.instModuleMulOppositeSubtypeMem_brauerGroup = Module.mk ⋯ ⋯

theorem TwoSidedIdeal.comap_comap {R : Type u_3} [Ring R] {S : Type u_5} {T : Type u_6} [Ring S] [Ring T] (f : R →+* S) (g : S →+* T) (I : TwoSidedIdeal T) : comap f (comap g I) = comap (g.comp f) I

def TwoSidedIdeal.orderIsoOfRingEquiv {R : Type u_3} [Ring R] {R' : Type u_4} [Ring R'] {F : Type u_5} [EquivLike F R R'] [RingEquivClass F R R'] (f : F) : TwoSidedIdeal R ≃o TwoSidedIdeal R'

Equations

• TwoSidedIdeal.orderIsoOfRingEquiv f = { toFun := TwoSidedIdeal.comap (↑f).symm, invFun := TwoSidedIdeal.comap ↑f, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem TwoSidedIdeal.injective_iff_ker_eq_bot {R : Type u_3} [Ring R] {R' : Type u_4} [Ring R'] {F : Type u_5} [FunLike F R R'] [RingHomClass F R R'] (f : F) : Function.Injective ⇑f ↔ ker f = ⊥

def TwoSidedIdeal.span' {R : Type u_3} [Ring R] (s : Set R) : TwoSidedIdeal R

Equations

• TwoSidedIdeal.span' s = TwoSidedIdeal.mk' {x : R | ∃ (ι : Type) (fin : Fintype ι) (xL : ι → R) (xR : ι → R) (y : ι → ↑s), x = ∑ i : ι, xL i * ↑(y i) * xR i} ⋯ ⋯ ⋯ ⋯ ⋯

theorem TwoSidedIdeal.mem_span'_iff_exists_fin {R : Type u_3} [Ring R] (s : Set R) (x : R) : x ∈ span' s ↔ ∃ (ι : Type) (x_1 : Fintype ι) (xL : ι → R) (xR : ι → R) (y : ι → ↑s), x = ∑ i : ι, xL i * ↑(y i) * xR i

theorem TwoSidedIdeal.mem_span_iff_exists_fin {R : Type u_3} [Ring R] (s : Set R) (x : R) : x ∈ span s ↔ ∃ (ι : Type) (x_1 : Fintype ι) (xL : ι → R) (xR : ι → R) (y : ι → ↑s), x = ∑ i : ι, xL i * ↑(y i) * xR i

theorem TwoSidedIdeal.mem_span_ideal_iff_exists_fin {R : Type u_3} [Ring R] (s : Ideal R) (x : R) : x ∈ span ↑s ↔ ∃ (ι : Type) (x_1 : Fintype ι) (xR : ι → R) (y : ι → ↥s), x = ∑ i : ι, ↑(y i) * xR i

theorem TwoSidedIdeal.span_le {R : Type u_3} [Ring R] {s : Set R} {I : TwoSidedIdeal R} : s ⊆ ↑I ↔ span s ≤ I

theorem TwoSidedIdeal.coe_bot_set {R : Type u_3} [Ring R] : ↑⊥ = {0}

theorem TwoSidedIdeal.coe_top_set {R : Type u_3} [Ring R] : ↑⊤ = Set.univ

instance TwoSidedIdeal.instNontrivial_brauerGroup (A : Type u) [Ring A] [Nontrivial A] : Nontrivial (TwoSidedIdeal A)

theorem IsSimpleRing.iff_eq_zero_or_injective' (A : Type u) [Ring A] (k : Type u_5) [CommRing k] [Algebra k A] [Nontrivial A] : IsSimpleRing A ↔ ∀ ⦃B : Type u⦄ [inst : Ring B] [inst_1 : Algebra k B] (f : A →ₐ[k] B), TwoSidedIdeal.ker f = ⊤ ∨ Function.Injective ⇑f