bot_pow

Mathlib.RingTheory.Ideal.Operations

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

English

For n ≠ 0, the n-th power of the bottom ideal is bottom: (⊥)^n = ⊥.

Русский

При n ≠ 0 степень нулевого идеала равна нулю: (⊥)^n = ⊥.

LaTeX

$$$(\\bot)^{n} = \\bot, \\ n \\neq 0$$$

Lean4

theorem bot_pow {n : ℕ} (hn : n ≠ 0) : (⊥ : Ideal R) ^ n = ⊥ :=
  Submodule.bot_pow hn

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

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

Разделы

Аффилиация

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