English
Among all nonzero p in the annihilating ideal annIdeal 𝕜 a, the degree of annIdealGenerator 𝕜 a is less than or equal to the degree of p; i.e., annIdealGenerator has minimal degree on the ideal’s nonzero elements.
Русский
Среди всех ненулевых p в аннигиляторном идеале annIdeal 𝕜 a степень annIdealGenerator 𝕜 a не превосходит степень p; то есть генератор имеет минимальную степень на ненулевых элементах идеала.
LaTeX
$$$\text{deg}(\operatorname{annIdealGenerator}_{\mathbb{k}}(a)) \le \text{deg}(p)$, for all nonzero $p \in \operatorname{annIdeal}_{\mathbb{k}}(a).$$$
Lean4
/-- The generator of the annihilating ideal has minimal degree among
the non-zero members of the annihilating ideal -/
theorem degree_annIdealGenerator_le_of_mem (a : A) (p : 𝕜[X]) (hp : p ∈ annIdeal 𝕜 a) (hpn0 : p ≠ 0) :
degree (annIdealGenerator 𝕜 a) ≤ degree p :=
degree_le_of_dvd (mem_iff_annIdealGenerator_dvd.1 hp) hpn0
