Theorems · Theorem · commutative algebra

Subsemiring.mem_closure_iff_exists_list

∀ {R : Type u_1} [inst : Semiring R] {s : Set R} {x : R},
  x ∈ Subsemiring.closure s ↔ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Defined in

Mathlib.Algebra.Ring.Subsemiring.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semiring