Mathlib Map

Theorems · Definition · ring theory

TwoSidedIdeal.asIdeal

{R : Type u_1} → [inst : Ring R] → TwoSidedIdeal R →o Ideal R

Every two-sided ideal is also a left ideal.

Defined in
Mathlib.RingTheory.TwoSidedIdeal.Operations
Cited by
13 results in Mathlib
Foundations
Depth 43 from the axioms · uses propext, Quot.sound
Assumes
Ring
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…IsLinearTopology.hasBasis_twoSidedIdeal · cited by 3IsLinearTopology.hasBasis…TwoSidedIdeal.asIdealOpposite · cited by 1TwoSidedIdeal.asIdealOppo…TwoSidedIdeal.asIdeal_jacobson · cited by 1TwoSidedIdeal.asIdeal_jac…TwoSidedIdeal.asIdeal_matrix · cited by 1TwoSidedIdeal.asIdeal_mat…TwoSidedIdeal.orderIsoIsTwoSided_apply_coe · cited by 1TwoSidedIdeal.orderIsoIsT…TwoSidedIdeal.jacobson_matrix · cited by 1TwoSidedIdeal.jacobson_ma…Ideal.asIdeal_toTwoSided · cited by 1Ideal.asIdeal_toTwoSidedIsLinearTopology.hasBasis_open_twoSidedIdeal · cited by 1IsLinearTopology.hasBasis…Ideal.toTwoSided_asIdeal · cited by 0Ideal.toTwoSided_asIdealTwoSidedIdeal.bot_asIdeal · cited by 0TwoSidedIdeal.bot_asIdealTwoSidedIdeal.orderIsoIdeal · cited by 0TwoSidedIdeal.orderIsoIde…TwoSidedIdeal.coe_asIdeal · cited by 0TwoSidedIdeal.coe_asIdealTwoSidedIdeal.mem_asIdeal · cited by 0TwoSidedIdeal.mem_asIdealSetLike.coe · cited by 8199SetLike.coeRing · cited by 7463RingIdeal · cited by 4748IdealOrderHom · cited by 934OrderHomTwoSidedIdeal · cited by 151TwoSidedIdealTwoSidedIdeal.asIdealCITED BYCITES

Cites5

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

Cited by17

Results whose statement or proof uses this declaration.