Theorems · Theorem · commutative algebra

Subring.exists_list_of_mem_closure

∀ {R : Type u_1} [inst : Ring R] {s : Set R} {x : R},
  x ∈ Subring.closure s → ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x

Defined in

Mathlib.Algebra.Ring.Subring.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Ring