isRadical_iff_pow_one_lt — Mathlib

English

For k>1, I is radical iff r^k ∈ I implies r ∈ I for all r in R.

Русский

Для k>1: I является радикалом тогда и только тогда, когда для всех r ∈ R из r^k ∈ I следует r ∈ I.

LaTeX

$$$$ I.IsRadical \iff \forall r \in R,\ r^k \in I \Rightarrow r \in I $$$$

Lean4

theorem isRadical_iff_pow_one_lt (k : ℕ) (hk : 1 < k) : I.IsRadical ↔ ∀ r, r ^ k ∈ I → r ∈ I :=
  ⟨fun h _r hr ↦ h ⟨k, hr⟩, fun h x ⟨n, hx⟩ ↦ k.pow_imp_self_of_one_lt hk _ (fun _ _ ↦ .inr ∘ I.smul_mem _) h n x hx⟩

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