coeffsIn_eq_span_monomial — Mathlib

English

The submodule coeffsIn σ M is exactly the span of all monomials monomial i m with m ∈ M and i ∈ σ →₀ ℕ.

Русский

Подмодуль coeffsIn σ M является точно порожденным множеством всех мономиалов monomial i m с m ∈ M и i ∈ σ →₀ ℕ.

LaTeX

$$$\\operatorname{coeffsIn}(\\sigma,M) = \\operatorname{span}_R\\{ \\operatorname{monomial}(i)\\,m \\,|\\, m \\in M, i \\in (\\sigma \\to\\₀ \\mathbb{N})\\}$$$

Lean4

theorem coeffsIn_eq_span_monomial : coeffsIn σ M = .span R ({monomial i m | (m ∈ M) (i : σ →₀ ℕ)}) := by
  classical
  refine le_antisymm ?_ <| Submodule.span_le.2 ?_
  · rintro p hp
    rw [p.as_sum]
    exact sum_mem fun i hi ↦ Submodule.subset_span ⟨_, hp i, _, rfl⟩
  · rintro _ ⟨m, hm, s, n, rfl⟩ i
    simp
    split <;> simp [hm]

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