coeffsIn — Mathlib

English

The submodule coeffsIn consists of polynomials whose coefficients lie in a given submodule M.

Русский

Подмодуль coeffsIn состоит из полиномов, коэффициенты которых лежат в заданном подмодуле M.

LaTeX

$$$ coeffsIn : Submodule R (MvPolynomial \\sigma S) \\text{ with carrier }\\{ p : MvPolynomial \\sigma S \\mid \\ \\forall i, p. coeff i \\in M \\}$.$$

Lean4

/-- The `R`-submodule of multivariate polynomials whose coefficients lie in a `R`-submodule `M`. -/
@[simps]
def coeffsIn : Submodule R (MvPolynomial σ S)
    where
  carrier := {p | ∀ i, p.coeff i ∈ M}
  add_mem' := by simp +contextual [add_mem]
  zero_mem' := by simp
  smul_mem' := by simp +contextual [Submodule.smul_mem]

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