pow_pos_iff

Mathlib.Algebra.Order.GroupWithZero.Canonical

URI: https://scilib.ai/kg/mathlib#pow_pos_iff

English

Let a be nonnegative, then for n ≠ 0, 0 < a^n iff 0 < a.

Русский

Пусть a неотрицательно; тогда при n ≠ 0: 0 < a^n ⇔ 0 < a.

LaTeX

$$$\\text{pow\_pos\_iff}(\\text{hn}: n \\neq 0) : 0 < a^n \\iff 0 < a$$$

Lean4

theorem pow_pos_iff (hn : n ≠ 0) : 0 < a ^ n ↔ 0 < a := by simp_rw [zero_lt_iff, pow_ne_zero_iff hn]

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

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

Разделы

Аффилиация

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