top_pow

Mathlib.Algebra.Order.Ring.WithTop

URI: https://scilib.ai/kg/mathlib#WithTop.top_pow

English

For any n > 0, (⊤ : WithTop α)^n = ⊤; moreover, n = 0 gives 1.

Русский

Для любого n > 0 вершина ⊤ в WithTop α в степени n равна ⊤; при n = 0 получается 1.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\ (n \\neq 0) \\Rightarrow (\\top : \\mathrm{WithTop} \\alpha)^n = \\top$$$

Lean4

@[simp]
theorem top_pow : ∀ {n : ℕ}, n ≠ 0 → (⊤ : WithTop α) ^ n = ⊤
  | _ + 1, _ => rfl

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

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

Разделы

Аффилиация

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