le_of_pow_le — Mathlib

English

If I^n ≤ P and P is prime, then I ≤ P (handling the case n=0 separately).

Русский

Если I^n ≤ P и P прост, тогда I ≤ P (обрабатывая случай n=0 отдельно).

LaTeX

$$$ I^n \le P \Rightarrow I \le P \quad (n \text{ arbitrary},\ P \text{ prime})$$$

Lean4

theorem le_of_pow_le {I P : Ideal R} [hP : P.IsPrime] {n : ℕ} (h : I ^ n ≤ P) : I ≤ P :=
  by
  by_cases hn : n = 0
  · rw [hn, pow_zero, one_eq_top] at h
    exact fun ⦃_⦄ _ ↦ h Submodule.mem_top
  · exact (pow_le_iff hn).mp h

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