optionEquivRight_C — Mathlib

English

For p in MvPolynomial(Option S1) and i, if i ≤ p.totalDegree, then totalDegree of the i-th coefficient of optionEquivLeft(p) plus i is ≤ p.totalDegree.

Русский

Для p ∈ MvPolynomial(Option S1) и i, если i ≤ totalDegree(p), то totalDegree(coef_i(optionEquivLeft(p))) + i ≤ totalDegree(p).

LaTeX

$$$\\text{If } i \\le p.totalDegree,\\; \\operatorname{totalDegree}( (\\operatorname{optionEquivLeft} R S_1\\;p).\\coeff i) + i \\le p.totalDegree$$$

Lean4

theorem optionEquivRight_C (r : R) : optionEquivRight R S₁ (C r) = C (Polynomial.C r) := by
  simp only [optionEquivRight_apply, aeval_C, algebraMap_apply, Polynomial.algebraMap_eq]

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