pow_smul_top_le — Mathlib

English

A variant formulation of the monotonicity of the powers of an ideal acting on the top submodule in a module setting.

Русский

Вариант формулировки монотонности степеней идеала, действующих на верхний подмодуль в модульном контексте.

LaTeX

$$$\forall m\le n:\; I^n \cdot \top \le I^m \cdot \top$$$

Lean4

theorem pow_smul_top_le {m n : ℕ} (h : m ≤ n) : (I ^ n • ⊤ : Submodule R M) ≤ I ^ m • ⊤ :=
  smul_mono_left (Ideal.pow_le_pow_right h)

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