zpow_pos_iff

Mathlib.Algebra.Order.Field.Power

URI: https://scilib.ai/kg/mathlib#Even.zpow_pos_iff

← MathLib Explorer

English

Let n be even and n ≠ 0. Then a^n > 0 iff a > 0.

Русский

Пусть n чётное и не равно нулю. Тогда a^n > 0 тогда и только тогда, когда a > 0.

LaTeX

$$For even n ≠ 0: $a^n>0 \\iff a>0$$$

Lean4

theorem zpow_pos_iff (hn : Even n) (h : n ≠ 0) : 0 < a ^ n ↔ a ≠ 0 :=
  by
  obtain ⟨k, rfl⟩ := hn
  rw [zpow_add' (by simp [em']), mul_self_pos, zpow_ne_zero_iff (by simpa using h)]

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

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

Разделы

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

Аффилиация

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