pow_right_mono — Mathlib

English

If I ≤ J then I^n ≤ J^n for all n ∈ ℕ (same as pow_right_mono).

Русский

Если I ≤ J, то I^n ≤ J^n для всех n∈ℕ (то же, что pow_right_mono).

LaTeX

$$$I \le J \Rightarrow I^n \le J^n$ for all $n \in \mathbb{N}$$$

Lean4

theorem pow_right_mono (e : I ≤ J) (n : ℕ) : I ^ n ≤ J ^ n := by
  induction n with
  | zero => rw [Submodule.pow_zero, Submodule.pow_zero]
  | succ _ hn =>
    rw [Submodule.pow_succ, Submodule.pow_succ]
    exact Ideal.mul_mono hn e

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