Theorems · Theorem · commutative algebra

Polynomial.Chebyshev.induct

∀ (motive : ℤ → Prop),
  motive 0 →
    motive 1 →
      (∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)) →
        (∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)) → ∀ (a : ℤ), motive a

Induction principle used for proving facts about Chebyshev polynomials.

Defined in

Mathlib.RingTheory.Polynomial.Chebyshev

Cited by

30 results in Mathlib

Foundations

Depth 48 from the axioms · uses propext, Quot.sound