pow_smul_le_pow_smul — Mathlib

English

Let i, j, k be natural numbers. Then the product of I^{i+k} with F.N(j) is contained in the product of I^k with F.N(i+j): I^{i+k} · F.N(j) ⊆ I^k · F.N(i+j).

Русский

Пусть i, j, k ∈ ℕ. Тогда I^{i+k} · F.N(j) ⊆ I^k · F.N(i+j).

LaTeX

$$$I^{i+k} \cdot F.N(j) \subseteq I^{k} \cdot F.N(i+j)$$$

Lean4

theorem pow_smul_le_pow_smul (i j k : ℕ) : I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j) :=
  by
  rw [add_comm, pow_add, mul_smul]
  exact smul_mono_right _ (F.pow_smul_le i j)

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