mem_adjoin_support — Mathlib

English

An element f in the monoid algebra R[M] lies in the subalgebra generated by the images of its support set.

Русский

Элемент f в алгебре монадной группы R[M] принадлежит подалгебре, порождаемой образами опоры f.

LaTeX

$$$f \\in \\mathrm{adjoin}_R\\bigl(\\mathrm{of}'_{R,M}''(f\\mathrm{.support})\\bigr)$$$

Lean4

/-- An element of `R[M]` is in the subalgebra generated by its support. -/
theorem mem_adjoin_support (f : R[M]) : f ∈ adjoin R (of' R M '' f.support) :=
  by
  suffices span R (of' R M '' f.support) ≤ Subalgebra.toSubmodule (adjoin R (of' R M '' f.support)) by
    exact this (mem_span_support f)
  rw [Submodule.span_le]
  exact subset_adjoin

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