instDistribMulAction — Mathlib

English

As above, the coefficient at g of a finite sum equals the sum of the coefficients at g.

Русский

Аналогично, коэффициент при g от конечной суммы равен сумме коэффициентов при g.

LaTeX

$$$$ (\sum i \in s \; x_i).coeff(g) = \sum_{i \in s} (x_i).coeff(g). $$$$

Lean4

instance : DistribMulAction R (HahnSeries Γ V) where
  smul := (· • ·)
  one_smul
    _ := by
    ext
    simp
  smul_zero
    _ := by
    ext
    simp
  smul_add _ _
    _ := by
    ext
    simp [smul_add]
  mul_smul _ _
    _ := by
    ext
    simp [mul_smul]

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