exists_pow_le_of_le_radical_of_fg_radical

English

If I ≤ J.radical and J.radical.FG, there exists n with I^n ≤ J.

Русский

Если I ≤ J.radical и J.radical FG, существует n, такое что I^n ≤ J.

LaTeX

$$I ≤ J.radical ∧ J.radical.FG ⇒ ∃ n, I^n ≤ J$$

Lean4

theorem exists_pow_le_of_le_radical_of_fg_radical {R : Type*} [CommSemiring R] {I J : Ideal R} (hIJ : I ≤ J.radical)
    (hJ : J.radical.FG) : ∃ k : ℕ, I ^ k ≤ J :=
  by
  obtain ⟨k, hk⟩ := J.exists_radical_pow_le_of_fg hJ
  use k
  calc
    I ^ k ≤ J.radical ^ k := Ideal.pow_right_mono hIJ _
    _ ≤ J := hk

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