Mathlib Map

Theorems · Definition · ring theory

Ideal.toTwoSided

{R : Type u_1} → [inst : Ring R] → (I : Ideal R) → [I.IsTwoSided] → TwoSidedIdeal R

Bundle an Ideal that is already two-sided as a TwoSidedIdeal.

Defined in
Mathlib.RingTheory.TwoSidedIdeal.Operations
Cited by
6 results in Mathlib
Foundations
Depth 42 from the axioms · uses propext
Assumes
RingIdeal.IsTwoSided
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

TwoSidedIdeal.jacobson · cited by 4TwoSidedIdeal.jacobsonTwoSidedIdeal.orderIsoIsTwoSided · cited by 3TwoSidedIdeal.orderIsoIsT…Ideal.asIdeal_toTwoSided · cited by 1Ideal.asIdeal_toTwoSidedTwoSidedIdeal.orderIsoIsTwoSided_symm_apply · cited by 0TwoSidedIdeal.orderIsoIsT…Ideal.toTwoSided.congr_simp · cited by 0toTwoSided.congr_simpIdeal.coe_toTwoSided · cited by 0Ideal.coe_toTwoSidedIdeal.mem_toTwoSided · cited by 0Ideal.mem_toTwoSidedIdeal.toTwoSided_asIdeal · cited by 0Ideal.toTwoSided_asIdealSetLike.coe · cited by 8199SetLike.coeRing · cited by 7463RingIdeal · cited by 4748IdealIdeal.IsTwoSided · cited by 179Ideal.IsTwoSidedTwoSidedIdeal · cited by 151TwoSidedIdealTwoSidedIdeal.mk' · cited by 8TwoSidedIdeal.mk'Ideal.toTwoSidedCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by8

Results whose statement or proof uses this declaration.