is_ideal_adic_pow — Mathlib

English

If J is adic, then its powers J^n are adic for all n > 0.

Русский

Если J адическая, то J^n адическая для всех n > 0.

LaTeX

$$$IsAdic J \\to (\\forall n>0, IsAdic(J^n))$$$

Lean4

theorem is_ideal_adic_pow {J : Ideal R} (h : IsAdic J) {n : ℕ} (hn : 0 < n) : IsAdic (J ^ n) :=
  by
  rw [isAdic_iff] at h ⊢
  constructor
  · intro m
    rw [← pow_mul]
    apply h.left
  · intro V hV
    obtain ⟨m, hm⟩ := h.right V hV
    use m
    refine Set.Subset.trans ?_ hm
    cases n
    · exfalso
      exact Nat.not_succ_le_zero 0 hn
    rw [← pow_mul, Nat.succ_mul]
    apply Ideal.pow_le_pow_right
    apply Nat.le_add_left

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