zero_epow

Mathlib.Data.ENat.Pow

URI: https://scilib.ai/kg/mathlib#ENat.zero_epow

← MathLib Explorer

English

If y ≠ 0, then ⊤^y = ⊤.

Русский

Если y ≠ 0, то ⊤^y = ⊤.

LaTeX

$$$ (y \neq ⊤) \rightarrow (⊤)^{y} = ⊤ $$$

Lean4

theorem zero_epow (h : y ≠ 0) : (0 : ℕ∞) ^ y = 0 := by
  induction y with
  | top => exact zero_epow_top
  | coe y => rwa [epow_natCast, pow_eq_zero_iff', eq_self 0, true_and, ← y.cast_ne_zero (R := ℕ∞)]

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

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

Разделы

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

Аффилиация

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