pow_eq_zero_iff

Mathlib.RingTheory.Nilpotent.Defs

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

← MathLib Explorer

English

If n ≠ 0, then x^n = 0 iff x = 0.

Русский

Если n ≠ 0, то x^n = 0 тогда и только тогда, когда x = 0.

LaTeX

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

Lean4

@[simp]
theorem pow_eq_zero_iff [MonoidWithZero R] [IsReduced R] {n : ℕ} (hn : n ≠ 0) : x ^ n = 0 ↔ x = 0 :=
  ⟨pow_eq_zero, fun h ↦ h.symm ▸ zero_pow hn⟩

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

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

Разделы

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

Аффилиация

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