English
A structured induction principle: to prove a property for Laurent polynomials, it suffices to prove it for constants and to show it is closed under sums and under multiplication by T n and T(-n).
Русский
Структурированная индукция по лаурентовским многочленам: достаточно доказать свойство для констант и показать его замкнутысть относительно сложения и умножения на T n и T(-n).
LaTeX
$$$\\text{Induction_on}(p, h_C, h_add, h_C_mul_T, h_C_mul_T_Z) : M(p) \\,$$$
Lean4
@[elab_as_elim]
protected theorem induction_on {M : R[T;T⁻¹] → Prop} (p : R[T;T⁻¹]) (h_C : ∀ a, M (C a))
(h_add : ∀ {p q}, M p → M q → M (p + q)) (h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T n) → M (C a * T (n + 1)))
(h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-n)) → M (C a * T (-n - 1))) : M p :=
by
have A : ∀ {n : ℤ} {a : R}, M (C a * T n) := by
intro n a
refine Int.induction_on n ?_ ?_ ?_
· simpa only [T_zero, mul_one] using h_C a
· exact fun m => h_C_mul_T m a
· exact fun m => h_C_mul_T_Z m a
have B : ∀ s : Finset ℤ, M (s.sum fun n : ℤ => C (p n) * T n) :=
by
apply Finset.induction
· convert h_C 0
simp only [Finset.sum_empty, map_zero]
· intro n s ns ih
rw [Finset.sum_insert ns]
exact h_add A ih
convert B p.support
ext a
simp_rw [← single_eq_C_mul_T]
rw [Finset.sum_apply', Finset.sum_eq_single a, single_eq_same]
· intro b _ hb
rw [single_eq_of_ne' hb]
· intro ha
rw [single_eq_same, notMem_support_iff.mp ha]
