multiset_sum_mem — Mathlib

English

Let S be an intermediate field of L over K. If every element of a multiset m of elements of L lies in S, then the sum of the elements of m lies in S.

Русский

Пусть S — промежутое поле L над K. Если каждый элемент multiseta m лежит в S, то сумма элементов m лежит в S.

LaTeX

$$$\forall m:\\Multiset L,\ (\forall a \in m,\ a ∈ S) \Rightarrow m.sum ∈ S$$$

Lean4

/-- Sum of a multiset of elements in an `IntermediateField` is in the `IntermediateField`. -/
protected theorem multiset_sum_mem (m : Multiset L) : (∀ a ∈ m, a ∈ S) → m.sum ∈ S :=
  multiset_sum_mem m

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