bot_pow

Mathlib.Algebra.Algebra.Operations

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

← MathLib Explorer

English

For all n ≠ 0, (⊥ : Submodule R A)^n = ⊥.

Русский

Для любого n > 0 нулевой подпмодуль в степени n равен нулю.

LaTeX

$$$ (\bot : Submodule R A)^{n} = \bot \quad (n \ne 0). $$$

Lean4

@[simp]
theorem bot_pow : ∀ {n : ℕ}, n ≠ 0 → (⊥ : Submodule R A) ^ n = ⊥
  | 1, _ => Submodule.pow_one _
  | n + 2, _ => by rw [Submodule.pow_succ, bot_pow n.succ_ne_zero, bot_mul]

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

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

Разделы

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

Аффилиация

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