pow_mem_of_pow_mem

Mathlib.RingTheory.Ideal.Defs

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

← MathLib Explorer

English

If a^m ∈ I and m ≤ n, then a^n ∈ I.

Русский

Если $a^m \in I$ и $m \le n$, то $a^n \in I$.

LaTeX

$$$\forall I\; (I: \text{Ideal } \alpha) \; \forall a \in \alpha, \forall m,n \in \mathbb{N}, \; (a^m \in I) \land (m \le n) \Rightarrow a^n \in I.$$$

Lean4

theorem pow_mem_of_pow_mem {m n : ℕ} (ha : a ^ m ∈ I) (h : m ≤ n) : a ^ n ∈ I :=
  by
  rw [← Nat.add_sub_of_le h, add_comm, pow_add]
  exact I.mul_mem_left _ ha

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

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

Разделы

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

Аффилиация

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