mul_X_mem_coeffsIn — Mathlib

English

Multiplying a polynomial p on the right by X s preserves membership in coeffsIn σ M: p · X s ∈ coeffsIn σ M iff p ∈ coeffsIn σ M.

Русский

Умножение многочлена p справа на X s сохраняет принадлежность к coeffsIn σ M: p · X s ∈ coeffsIn σ M тогда и только тогда, когда p ∈ coeffsIn σ M.

LaTeX

$$$p \\cdot X\\,s \\in \\operatorname{coeffsIn}(\\sigma,M) \\iff p \\in \\operatorname{coeffsIn}(\\sigma,M)$$$

Lean4

@[simp]
theorem mul_X_mem_coeffsIn : p * X s ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M := by
  simpa [-mul_monomial_mem_coeffsIn] using mul_monomial_mem_coeffsIn (i := .single s 1)

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