pow_succ_lt_pow — Mathlib

English

For a nonzero prime ideal P in a Dedekind domain A and any natural i, the inclusion P^(i+1) < P^i holds; i.e., powers of a nonzero prime ideal form a strictly descending chain.

Русский

Для непустого простого идеала P в области Дедекуда A и любого натурального i вложение P^(i+1) < P^i выполняется; степени простого идеала образуют строго нисходящую последовательность.

LaTeX

$$$P^{i+1} < P^i$$$

Lean4

theorem pow_succ_lt_pow {P : Ideal A} [P_prime : P.IsPrime] (hP : P ≠ ⊥) (i : ℕ) : P ^ (i + 1) < P ^ i :=
  lt_of_le_of_ne (Ideal.pow_le_pow_right (Nat.le_succ _))
    (mt (pow_inj_of_not_isUnit (mt Ideal.isUnit_iff.mp P_prime.ne_top) hP).mp i.succ_ne_self)

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