Theorems · Theorem · commutative algebra

MvPolynomial.IsWeightedHomogeneous.induction_on

∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} {m : M}
  {motive : (p : MvPolynomial σ R) → MvPolynomial.IsWeightedHomogeneous w p m → Prop},
  motive 0 ⋯ →
    (∀ (p q : MvPolynomial σ R) (hp : MvPolynomial.IsWeightedHomogeneous w p m)
        (hq : MvPolynomial.IsWeightedHomogeneous w q m), motive p hp → motive q hq → motive (p + q) ⋯) →
      (∀ (d : σ →₀ ℕ) (r : R) (hr : (Finsupp.weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯) →
        ∀ {p : MvPolynomial σ R} (hp : MvPolynomial.IsWeightedHomogeneous w p m), motive p hp

Induction principle for weighted homogeneous polynomials.

Defined in

Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoid