coeffs_C — Mathlib

English

The coefficients of the constant polynomial C r are given by: if r = 0 then ∅ else { r }.

Русский

Коэффициенты константного полинома C r равны: если r = 0, то ∅, иначе { r }.

LaTeX

$$$ [DecidableEq R] \\Rightarrow (C(\\sigma := \\sigma) \\; r).\\mathrm{coeffs} = \\begin{cases} \\emptyset, & \\text{if } r = 0 \\\\ {r}, & \\text{otherwise} \\end{cases}$. $$

Lean4

theorem coeffs_C [DecidableEq R] (r : R) : (C (σ := σ) r).coeffs = if r = 0 then ∅ else { r } := by
  classical aesop (add simp mem_coeffs_iff)

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