map_eq_zero — Mathlib

English

The map sends a constant a to the constant series with coefficient f a: map f (C a) = C (f a).

Русский

Отображение отправляет константный элемент a в константный ряд с коэффициентом f a: map f (C a) = C (f a).

LaTeX

$$$\\mathrm{map}\\ f\\ (C a) = C (f a)$$$

Lean4

@[simp]
theorem map_eq_zero {S : Type*} [DivisionSemiring R] [Semiring S] [Nontrivial S] (φ : MvPowerSeries σ R) (f : R →+* S) :
    φ.map f = 0 ↔ φ = 0 := by
  simp only [MvPowerSeries.ext_iff]
  congr! with n
  simp

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