mem_reesAlgebra_iff — Mathlib

English

For a polynomial f, membership in the Rees algebra of I is equivalent to the coefficient-wise condition f_i ∈ I^i for all i.

Русский

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

LaTeX

$$$f \in \mathrm{reesAlgebra}(I) \iff \forall i, f.i \in I^{i}$$$

Lean4

theorem mem_reesAlgebra_iff (f : R[X]) : f ∈ reesAlgebra I ↔ ∀ i, f.coeff i ∈ I ^ i :=
  Iff.rfl

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