mem_reesAlgebra_iff_support — Mathlib

English

A polynomial f lies in the Rees algebra I if and only if every coefficient with index i that is in the support satisfies f_i ∈ I^i.

Русский

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

LaTeX

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

Lean4

theorem mem_reesAlgebra_iff_support (f : R[X]) : f ∈ reesAlgebra I ↔ ∀ i ∈ f.support, f.coeff i ∈ I ^ i :=
  by
  apply forall_congr'
  intro a
  rw [mem_support_iff, Iff.comm, Classical.imp_iff_right_iff, Ne, ← imp_iff_not_or]
  exact fun e => e.symm ▸ (I ^ a).zero_mem

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