induction — Mathlib

English

For every a, (0 : Poly α) a = 0.

Русский

Для каждого a верно, что (0 : Poly α) a = 0.

LaTeX

$$$$ (0 : Poly \\alpha)(a) = 0 $$$$

Lean4

theorem induction {C : Poly α → Prop} (H1 : ∀ i, C (proj i)) (H2 : ∀ n, C (const n)) (H3 : ∀ f g, C f → C g → C (f - g))
    (H4 : ∀ f g, C f → C g → C (f * g)) (f : Poly α) : C f :=
  by
  obtain ⟨f, pf⟩ := f
  induction pf with
  | proj => apply H1
  | const => apply H2
  | sub _ _ ihf ihg => apply H3 _ _ ihf ihg
  | mul _ _ ihf ihg => apply H4 _ _ ihf ihg

Похожие утверждения