monomial_mem_coeffsIn — Mathlib

English

The coefficient of the monomial monomial i in coeffsIn is 0 when the index is not in the support.

Русский

Коэффициент монома в coeffsIn равен 0, если индекс не входит в опору.

LaTeX

$$$ monomial(i).coeff == 0 \\Rightarrow i \\\\in \\mathrm{Supp}(...) $$$

Lean4

@[simp]
theorem monomial_mem_coeffsIn : monomial i x ∈ coeffsIn σ M ↔ x ∈ M := by
  classical
  simp only [mem_coeffsIn, coeff_monomial]
  exact ⟨fun h ↦ by simpa using h i, fun hs j ↦ by split <;> simp [hs]⟩

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