filterLinearMap — Mathlib

English

The operation filter p defines a linear map on the DFinsupp family.

Русский

Операция фильтрации по p определяет линейное отображение на семействе DFinsupp.

LaTeX

$$$$ \\mathrm{filterLinearMap}: (p) \\to_{\\\\ell} (DFinsupp \\; \\beta_i) $$$$

Lean4

/-- `DFinsupp.filter` as a `LinearMap`. -/
@[simps]
def filterLinearMap [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] (p : ι → Prop) [DecidablePred p] :
    (Π₀ i, β i) →ₗ[γ] Π₀ i, β i where
  toFun := filter p
  map_add' := filter_add p
  map_smul' := filter_smul p

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