coe_eq_one_iff — Mathlib

English

Let R be a semiring and φ a polynomial in R[X]. When φ is viewed as a formal power series, it equals 1 if and only if φ is the constant polynomial 1.

Русский

Пусть R — полукольцо и φ ∈ R[X]. Рассматривая φ как ряд степеней, получаем равенство φ = 1 тогда и только если φ = 1 как полином.

LaTeX

$$$(\\varphi : \\mathrm{PowerSeries}(R)) = 1 \\iff \\varphi = 1$$$

Lean4

@[simp]
theorem coe_eq_one_iff : (φ : PowerSeries R) = 1 ↔ φ = 1 := by rw [← coe_one, coe_inj]

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