map_single — Mathlib

English

For any Zero-typed target S and a map f, mapping a Hahn series with a single-term coefficient commutes with mapping the coefficients.

Русский

Для отображения f сохраняется совместимость отображения с единичным членом ряда Ханна.

LaTeX

$$[simp] map_single : (single a r).map f = single a (f r)$$

Lean4

@[simp]
protected theorem map_single [Zero S] (f : ZeroHom R S) : (single a r).map f = single a (f r) :=
  by
  ext g
  by_cases h : g = a <;> simp [h]

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