mem_coeffsIn_iff_coeffs_subset — Mathlib

English

A polynomial p lies in coeffsIn σ M if and only if all coefficients that appear in p lie in M; equivalently, p.coeffs is a subset of M.

Русский

Полином p принадлежит coeffsIn σ M тогда и только тогда, когда все коэффициенты в p принадлежат M; эквивалентно p.coeffs ⊆ M.

LaTeX

$$$p \\in \\operatorname{coeffsIn}(\\sigma,M) \\iff (p.{\\text{coeffs}} : \\operatorname{Set} S) \\subseteq M$$$

Lean4

theorem mem_coeffsIn_iff_coeffs_subset : p ∈ coeffsIn σ M ↔ (p.coeffs : Set S) ⊆ M :=
  by
  simp only [mem_coeffsIn, coeffs, Finset.coe_image, image_subset_iff]
  refine ⟨fun h x _ ↦ h x, fun h i ↦ ?_⟩
  by_cases hp : i ∈ p.support
  · exact h hp
  · convert M.zero_mem
    simpa using hp

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