cast_negOnePow_natCast

Mathlib.Algebra.Ring.NegOnePow

URI: https://scilib.ai/kg/mathlib#Int.cast_negOnePow_natCast

← MathLib Explorer

English

In any ring R, negOnePow n equals (-1)^n.

Русский

Во всяком кольце R выполнено: negOnePow n = (-1)^n.

LaTeX

$$$$\\operatorname{negOnePow}(n) = (-1)^n \\text{ in } R$$$$

Lean4

theorem cast_negOnePow_natCast (R : Type*) [Ring R] (n : ℕ) : negOnePow n = (-1 : R) ^ n := by
  obtain ⟨k, rfl | rfl⟩ := Nat.even_or_odd' n <;> simp [pow_succ, pow_mul]

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

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

Разделы

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

Аффилиация

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