multiset_prod_span_singleton — Mathlib

English

For a multiset m of elements of R, the product of principal spans along m equals the principal span of the product of all elements of m.

Русский

Для мультисета элементов R произведение спанов по мультисету равно спану произведения всех элементов мультисета.

LaTeX

$$$\\prod_{x\\in m} \\operatorname{span}(\{x\\}) = \\operatorname{span}\\left(\\{\\prod_{x\\in m} x\\}\\right)$$$

Lean4

@[simp]
theorem multiset_prod_span_singleton (m : Multiset R) :
    (m.map fun x => Ideal.span { x }).prod = Ideal.span ({Multiset.prod m} : Set R) :=
  Multiset.induction_on m (by simp) fun a m ih => by
    simp only [Multiset.map_cons, Multiset.prod_cons, ih, ← Ideal.span_singleton_mul_span_singleton]

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