Theorems · Theorem · commutative algebra

Algebra.adjoin_singleton_induction

∀ (R : Type u) {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A)
  {M : ↥R[x] → Prop} (a : ↥R[x]), (∀ (p : Polynomial R), M ⟨(Polynomial.aeval x) p, ⋯⟩) → M a

Proving a fact about a : adjoin R {x} is the same as proving it for aeval x p where pis an arbitrary polynomial.

Defined in

Mathlib.RingTheory.Adjoin.Polynomial.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebra