annIdealGenerator_eq_zero_iff — Mathlib

English

The equation annIdealGenerator 𝕜 a = 0 is equivalent to annIdeal 𝕜 a = ⊥, i.e., the annihilating ideal is the zero ideal exactly when its chosen generator is 0.

Русский

Уравнение annIdealGenerator 𝕜 a = 0 эквивалентно annIdeal 𝕜 a = ⊥, то есть аннигиляционный идеал равен нулю тогда и только тогда, когда выбранный генератор равен 0.

LaTeX

$$$ annIdealGenerator\ 𝕜 a = 0 \iff annIdeal\ 𝕜 a = \bot $$$

Lean4

@[simp]
theorem annIdealGenerator_eq_zero_iff {a : A} : annIdealGenerator 𝕜 a = 0 ↔ annIdeal 𝕜 a = ⊥ := by
  simp only [annIdealGenerator, mul_eq_zero, IsPrincipal.eq_bot_iff_generator_eq_zero, Polynomial.C_eq_zero,
    inv_eq_zero, Polynomial.leadingCoeff_eq_zero, or_self_iff]

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