X_mul_mem_coeffsIn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem X_mul_mem_coeffsIn : X s * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M := by simp [mul_comm]

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