coeffsIn_le — Mathlib

English

For any submodule N of MvPolynomial σ S, coeffsIn σ M ≤ N if and only if every monomial monomial i m with m ∈ M lies in N for all i.

Русский

Для любого подмодуля N полиномов MvPolynomial σ S верно, что coeffsIn σ M ≤ N тогда и только тогда, когда для каждого m ∈ M и каждого i выполняется monomial i m ∈ N.

LaTeX

$$$\\operatorname{coeffsIn}(\\sigma,M) \\le N \\iff \\forall m \\in M, \\forall i, \\operatorname{monomial}(i)\\,m \\in N$$$

Lean4

theorem coeffsIn_le {N : Submodule R (MvPolynomial σ S)} : coeffsIn σ M ≤ N ↔ ∀ m ∈ M, ∀ i, monomial i m ∈ N := by
  simp [coeffsIn_eq_span_monomial, Submodule.span_le, Set.subset_def, forall_swap (α := MvPolynomial σ S)]

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