toLaurent_comp_C — Mathlib

English

A variant of the induction principle: to prove a property for Laurent polynomials, it suffices to show it for C a and closed under addition and T n operations.

Русский

Вариант принципа индукции: для лаурентовских многочленов достаточно доказать свойство для C a и замкнутость под сложение и операции T n.

LaTeX

$$$\\text{InductionOn}'(p, \\text{C_mul_T})$ expresses: for motive p, if p is built from C a and T n by sums and products, then p has the property.$$

Lean4

@[simp]
theorem _root_.Polynomial.toLaurent_comp_C : toLaurent (R := R) ∘ Polynomial.C = C :=
  funext Polynomial.toLaurent_C

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