pow_right_strictAnti — Mathlib

English

The same strict monotonicity result for left multiplication by a fixed nonzero ideal on the lattice of ideals.

Русский

Та же строгая монотонность левого умножения на фиксированный ненулевой идеал на решетке идеалов.

LaTeX

$$$\mathrm{PosMulStrictMono}(\mathrm{Ideal}(A))$$$

Lean4

theorem pow_right_strictAnti (I : Ideal A) (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) : StrictAnti (I ^ · : ℕ → Ideal A) :=
  strictAnti_nat_of_succ_lt fun e =>
    Ideal.dvdNotUnit_iff_lt.mp ⟨pow_ne_zero _ hI0, I, mt isUnit_iff.mp hI1, pow_succ I e⟩

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