Theorems · Theorem · field theory

LaurentPolynomial.reduce_to_polynomial_of_mul_T

∀ {R : Type u_1} [inst : Semiring R] (f : LaurentPolynomial R) {Q : LaurentPolynomial R → Prop},
  (∀ (f : Polynomial R), Q (Polynomial.toLaurent f)) →
    (∀ (f : LaurentPolynomial R), Q (f * LaurentPolynomial.T 1) → Q f) → Q f

Suppose that Q is a statement about Laurent polynomials such that * Q is true on ordinary polynomials; * Q (f * T) implies Q f; it follow that Q is true on all Laurent polynomials.

Defined in

Mathlib.Algebra.Polynomial.Laurent

Cited by

0 results in Mathlib

Foundations

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

Assumes

Semiring