monomial_mem — Mathlib

English

For any polynomial ring, a monomial of degree i with coefficient r lies in the Rees algebra I if and only if r ∈ I^i.

Русский

Для монома степени i с коэффициентом r выполнение принадлежности Rees-алгебре I эквивалентно тому, что r ∈ I^i.

LaTeX

$$$\text{monomial } i\, r \in \mathrm{reesAlgebra}(I) \iff r \in I^{i}$$$

Lean4

theorem monomial_mem {I : Ideal R} {i : ℕ} {r : R} : monomial i r ∈ reesAlgebra I ↔ r ∈ I ^ i := by
  simp +contextual [mem_reesAlgebra_iff_support, coeff_monomial, ← imp_iff_not_or]

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