add_sigma — Mathlib

English

Definition: the sigma operation is additive in the left argument: (s + t).sigma u = s.sigma u + t.sigma u.

Русский

Определение: сигма-операция аддитивна по левому аргументу: (s + t).sigma u = s.sigma u + t.sigma u.

LaTeX

$$$(s + t).\sigma u = s.\sigma u + t.\sigma u$$$

Lean4

@[simp]
theorem add_sigma (s t : Multiset α) (u : ∀ a, Multiset (σ a)) : (s + t).sigma u = s.sigma u + t.sigma u := by
  simp [Multiset.sigma]

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