mul_monomial_mem_coeffsIn — Mathlib

English

A monomial with index i and coefficient x lies in coeffsIn iff x lies in M.

Русский

Мономиал с индексом i и коэффициентом x лежит в coeffsIn тогда и только тогда, когда x ∈ M.

LaTeX

$$$ monomial(i)\\, x \\in coeffsIn(\\sigma, M) \\iff x \\in M. $$$

Lean4

@[simp]
theorem mul_monomial_mem_coeffsIn : p * monomial i 1 ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M := by
  classical
  simp only [mem_coeffsIn, coeff_mul_monomial']
  constructor
  · rintro hp j
    simpa using hp (j + i)
  · rintro hp i
    split <;> simp [hp]

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