radical_pow — Mathlib

English

Let I be an ideal in a commutative semiring R. For any n ≥ 1 with n ≠ 0, the radical of I^n equals the radical of I: √(I^n) = √I.

Русский

Пусть I — идеал в коммутативной полугруппе R. При любом n ≥ 1, n ≠ 0 радикал I^n равен радикалу I: √(I^n) = √I.

LaTeX

$$$ \forall I \ (n \ge 1),\ n \neq 0:\quad \operatorname{radical}(I^n) = \operatorname{radical}(I) $$$

Lean4

theorem radical_pow : ∀ {n}, n ≠ 0 → radical (I ^ n) = radical I
  | 1, _ => by simp
  | n + 2, _ => by rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]

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