pow_lt_self — Mathlib

English

For a fixed nonzero ideal I, the sequence I^e is strictly decreasing for e ≥ 2 in a Dedekind domain with nontrivial I.

Русский

Для фиксированного ненулевого идеала I последовательность I^e строго убывает при e ≥ 2 в детерминантном домене, если I не ноль и не единица.

LaTeX

$$$\forall I \,(I \neq 0) \land (I \neq 1)\ , \forall e\ge 2:\ I^e < I$$$

Lean4

theorem pow_lt_self (I : Ideal A) (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (e : ℕ) (he : 2 ≤ e) : I ^ e < I :=
  by
  convert I.pow_right_strictAnti hI0 hI1 he
  dsimp only
  rw [pow_one]

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