Induction on leading coefficient of polynomial

Stream: Is there code for X?

[Violeta Hernández]

Do we have anything like this?

import Mathlib.Algebra.Polynomial.Degree.Operations

variable {R : Type*} [Ring R]
open Polynomial

theorem Polynomial.monomial_induction {motive : R[X] → Prop} (zero : motive 0)
    (add : ∀ a n q, degree q < .some n → motive q → motive (C a * X ^ n + q)) (p : R[X]) :
    motive p := by
  induction hn : p.degree using WellFoundedLT.induction generalizing p with | ind n IH
  cases n with
  | bot => simp_all
  | coe n =>
    rw [← _root_.add_sub_cancel (C (p.coeff n) * X ^ n) p]
    have hpn : (p - C (p.coeff n) * X ^ n).degree < .some n := by
      rw [← hn]
      apply degree_sub_lt
      · simpa [degree_C_mul_X_pow _ (p.coeff_ne_zero_of_eq_degree hn)]
      · aesop
      · rw [leadingCoeff, natDegree_eq_of_degree_eq_some hn]
        simp
    exact add _ _ _ hpn (IH _ hpn _ rfl)

[Violeta Hernández]

I was only able to prove it for Ring R, but I think it should be true when only Semiring R.

[Christian Merten]

Is docs#Polynomial.induction_on not good enough?

[Violeta Hernández]

Nope, adding arbitrary polynomials is too strong for what I want to do

[Ruben Van de Velde]

Is the point of the subtraction to remove the leading term? That seems like something we should have a def for

[Ruben Van de Velde]

Eraselead

[Ruben Van de Velde]

docs#Polynomial.eraseLead , that is

[Violeta Hernández]

Yeah, that's much better

theorem monomial_induction {R} [Semiring R] {motive : R[X] → Prop} (zero : motive 0)
    (add : ∀ a n q, degree q < .some n → motive q → motive (C a * X ^ n + q)) (p : R[X]) :
    motive p := by
  induction hn : p.degree using WellFoundedLT.induction generalizing p with | ind n IH
  cases n with
  | bot => simp_all
  | coe n =>
    rw [← eraseLead_add_C_mul_X_pow p, add_comm]
    have hp₀ : p ≠ 0 := by aesop
    have hpn : p.eraseLead.degree < .some n := hn ▸ degree_eraseLead_lt hp₀
    apply add _ _ _ ((degree_eraseLead_lt hp₀).trans_eq _) (IH _ hpn _ rfl)
    rw [hn, natDegree_eq_of_degree_eq_some hn]

[Yakov Pechersky]

How about docs#Polynomial.degree_pos_induction_on

[Violeta Hernández]

That doesn't work for what I want either

[Violeta Hernández]

I do very specifically need to induct on the leading term