isIdempotentElem_iff_eq_bot_or_top

English

For a finitely generated ideal I in a domain, I is idempotent if and only if I is either the zero ideal or the whole ring.

Русский

Для конечнопоргенитированного идeала I в области кольца верно: I идempotent ⇔ I = 0 или I = R.

LaTeX

$$$\text{FG}(I) \Rightarrow (I^2 = I \iff I = \{0\} \lor I = R)$$$

Lean4

theorem isIdempotentElem_iff_eq_bot_or_top {R : Type*} [CommRing R] [IsDomain R] (I : Ideal R) (h : I.FG) :
    IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤ := by
  constructor
  · intro H
    obtain ⟨e, he, rfl⟩ := (I.isIdempotentElem_iff_of_fg h).mp H
    simp only [Ideal.submodule_span_eq, Ideal.span_singleton_eq_bot]
    apply Or.imp id _ (IsIdempotentElem.iff_eq_zero_or_one.mp he)
    rintro rfl
    simp
  · rintro (rfl | rfl) <;> simp [IsIdempotentElem]

Похожие утверждения