Theorems · Theorem · commutative algebra

MvPolynomial.induction_on

∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R),
  (∀ (a : R), motive (MvPolynomial.C a)) →
    (∀ (p q : MvPolynomial σ R), motive p → motive q → motive (p + q)) →
      (∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * MvPolynomial.X n)) → motive p

Analog of Polynomial.induction_on. If a property holds for any constant polynomial and is preserved under addition and multiplication by variables then it holds for all multivariate polynomials.

Defined in

Mathlib.Algebra.MvPolynomial.Basic

Cited by

43 results in Mathlib

Foundations

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

Assumes

CommSemiring