constantCoeff_C — Mathlib

English

The coeffs of C r can be described as in coeffs_C: either empty if r = 0, or the singleton { r } otherwise.

Русский

Для C r коэффициенты задаются как в coeffs_C: пусто, если r = 0; иначе — { r }.

LaTeX

$$$ (C(\\sigma := \\sigma) r).\\mathrm{coeffs} = \\begin{cases} \\emptyset, & r = 0 \\\\ { r }, & r \\neq 0 \\end{cases} $.$$

Lean4

@[simp]
theorem constantCoeff_C (r : R) : constantCoeff (C r : MvPolynomial σ R) = r := by classical simp [constantCoeff_eq]

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