pow_le_iff — Mathlib

English

If P is prime, then for any I, n ≠ 0, I^n ≤ P iff I ≤ P.

Русский

Если P прост, то для любого I, n ≠ 0, I^n ≤ P эквивалентно I ≤ P.

LaTeX

$$$ I ^ n \le P \iff I \le P \quad (n \neq 0,\ P \text{ prime})$$$

Lean4

theorem pow_le_iff {I P : Ideal R} [hP : P.IsPrime] {n : ℕ} (hn : n ≠ 0) : I ^ n ≤ P ↔ I ≤ P :=
  by
  have h : (Multiset.replicate n I).prod ≤ P ↔ _ := hP.multiset_prod_le
  simp_rw [Multiset.prod_replicate, Multiset.mem_replicate, ne_eq, hn, not_false_eq_true, true_and, exists_eq_left] at h
  exact h

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