Theorems · Definition · commutative algebra
IdealFilter
(A : Type u_1) → [Ring A] → Type u_1
IdealFilter A is the type of Order.PFilters on the lattice of ideals of A.
- Defined in
- Mathlib.RingTheory.IdealFilter.Basic
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Idealproof · cited by 4,748
- Order.PFilterproof · cited by 32
Cited by30
Results whose statement or proof uses this declaration.
- IdealFilter.IsTorsionQuotstatement and proof · cited by 9
- IdealFilter.IsUniformstatement · cited by 4
- IdealFilter.ringFilterBasisstatement and proof · cited by 2
- WithIdealFilterstatement and proof · cited by 2
- IdealFilter.IsTorsionQuot.anti_rightstatement and proof · cited by 2
- IdealFilter.IsTorsionQuot.mono_leftstatement and proof · cited by 2
- WithIdealFilter.idealSetstatement and proof · cited by 2
- IdealFilter.IsGabrielstatement · cited by 2
- IdealFilter.isTorsionQuot_selfstatement and proof · cited by 2
- IdealFilter.IsGabriel.gabriel_closedstatement and proof · cited by 1
- IdealFilter.IsTorsionQuot.infstatement and proof · cited by 1
- WithIdealFilter.mem_nhds_iffstatement and proof · cited by 1