Theorems · Inductive type · ring theory
TwoSidedIdeal
(R : Type u_1) → [NonUnitalNonAssocRing R] → Type u_1
A two-sided ideal of a ring R is a subset of R that contains 0 and is closed under addition,
negation, and absorbs multiplication on both sides.
- Defined in
- Mathlib.RingTheory.TwoSidedIdeal.Basic
- Cited by
- 151 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- NonUnitalNonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NonUnitalNonAssocRingstatement · cited by 354
Cited by187
Results whose statement or proof uses this declaration.
- TwoSidedIdeal.ringConstatement and proof · cited by 40
- TwoSidedIdeal.asIdealstatement and proof · cited by 13
- TwoSidedIdeal.matrixstatement and proof · cited by 10
- TwoSidedIdeal.mem_iffstatement and proof · cited by 9
- TwoSidedIdeal.spanstatement · cited by 9
- compactlySupportedstatement · cited by 8
- TwoSidedIdeal.mk'statement · cited by 8
- TwoSidedIdeal.mul_mem_leftstatement and proof · cited by 8
- TwoSidedIdeal.mul_mem_rightstatement and proof · cited by 7
- Ideal.toTwoSidedstatement · cited by 6
- TwoSidedIdeal.kerstatement · cited by 6
- TwoSidedIdeal.mem_span_iffstatement and proof · cited by 6