contentIdeal_eq_bot_iff — Mathlib

English

For any polynomial p in R[X], contentIdeal(p) = ⊥ iff p = 0.

Русский

Для любого p ∈ R[X], contentIdeal(p) = ⊥ тогда и только тогда p = 0.

LaTeX

$$$(p\, .contentIdeal = \bot) \iff (p = 0)$$$

Lean4

@[simp]
theorem contentIdeal_eq_bot_iff : p.contentIdeal = ⊥ ↔ p = 0 :=
  by
  simp only [contentIdeal_def, span_eq_bot]
  refine ⟨?_, fun h ↦ by simp [h]⟩
  contrapose!
  exact fun h ↦ ⟨p.leadingCoeff, coeff_mem_coeffs (leadingCoeff_ne_zero.mpr h), leadingCoeff_ne_zero.mpr h⟩

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