Theorems · Theorem · commutative algebra
Ideal.isIdempotentElem_iff_of_fg
∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), I.FG → (IsIdempotentElem I ↔ ∃ e, IsIdempotentElem e ∧ I = R ∙ e)A finitely generated idempotent ideal is generated by an idempotent element
- Defined in
- Mathlib.RingTheory.Ideal.IdempotentFG
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- Idealstatement and proof · cited by 4,748
- mul_commproof · cited by 2,262
- Submodule.spanstatement and proof · cited by 1,504
- Ideal.spanproof · cited by 948
- Eq.geproof · cited by 375
- smul_eq_mulproof · cited by 357
- IsIdempotentElemstatement and proof · cited by 217
- Ideal.FGstatement and proof · cited by 99
- IsIdempotentElem.eqproof · cited by 42
- Submodule.span_singleton_le_iff_memproof · cited by 21
Cited by5
Results whose statement or proof uses this declaration.
- Algebra.FormallyUnramified.iff_exists_tensorProductproof · cited by 2
- Algebra.FormallyUnramified.exists_algEquiv_prodproof · cited by 1
- Algebra.IsStandardEtale.of_surjectiveproof · cited by 1
- Ideal.Pure.of_isIdempotentElemproof · cited by 0
- Ideal.isIdempotentElem_iff_eq_bot_or_topproof · cited by 0