Theorems · Theorem · ring theory

OrthogonalIdempotents.lift_of_isNilpotent_ker_aux

∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    ∀ {n : ℕ} {e : Fin n → S},
      OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Defined in

Mathlib.RingTheory.Idempotents

Cited by

1 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingRing