one_epow

Mathlib.Data.ENat.Pow

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

English

For any x and y, x^(y:ℕ∞) = x^y

Русский

Для любого x и y, x^(y:ℕ∞) = x^y

LaTeX

$$$ x^{(y : \mathbb{N}_\infty)} = x^{y} $$$

Lean4

@[simp]
theorem one_epow : (1 : ℕ∞) ^ y = 1 := by
  induction y with
  | top => rfl
  | coe y => rw [epow_natCast, one_pow]

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

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

Разделы

Аффилиация

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