Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Ideal.span_eq_top_of_span_image_evalRingHom

∀ {ι : Type u_2} {R : ι → Type u_1} [inst : (i : ι) → CommRing (R i)] (s : Set ((i : ι) → R i)),
  s.Finite → (∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x => R x) i) '' s) = ⊤) → Ideal.span s = ⊤

Defined in

Mathlib.AlgebraicGeometry.PointsPi

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing