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