pow_eq_zero

Mathlib.RingTheory.Nilpotent.Defs

URI: https://scilib.ai/kg/mathlib#IsReduced.pow_eq_zero

English

For any nonzero exponent n, x^n = 0 implies x = 0, i.e., if n ≠ 0 then x^n = 0 ⇔ x = 0.

Русский

Для любого n ≠ 0 верно: x^n = 0 тогда и только тогда, когда x = 0.

LaTeX

$$$\forall n \,(n \neq 0) \Rightarrow (x^n = 0 \iff x = 0)$$$

Lean4

theorem pow_eq_zero [Zero R] [Pow R ℕ] [IsReduced R] {n : ℕ} (h : x ^ n = 0) : x = 0 :=
  IsReduced.eq_zero x ⟨n, h⟩

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

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

Разделы

Аффилиация

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