pow_le_self

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.pow_le_self

← MathLib Explorer

English

If I ≤ J then I^n ≤ J^n for all n ∈ ℕ.

Русский

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

LaTeX

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

Lean4

theorem pow_le_self {n : ℕ} (hn : n ≠ 0) : I ^ n ≤ I :=
  calc
    I ^ n ≤ I ^ 1 := pow_le_pow_right (Nat.pos_of_ne_zero hn)
    _ = I := Submodule.pow_one _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru