pow_eq_zero

Mathlib.Algebra.GroupWithZero.Basic

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

← MathLib Explorer

English

In a MonoidWithZero with NoZeroDivisors, if a^n = 0 then a = 0 for any n.

Русский

В моноиде с нулём и без делителей нуля, если a^n = 0, то a = 0.

LaTeX

$$$$ \forall n \in \mathbb{N},\ a^{n} = 0 \Rightarrow a = 0 $$$$

Lean4

theorem pow_eq_zero : ∀ {n}, a ^ n = 0 → a = 0
  | 0, ha => by simpa using congr_arg (a * ·) ha
  | n + 1, ha => by rw [pow_succ, mul_eq_zero] at ha; exact ha.elim pow_eq_zero id

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

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

Разделы

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

Аффилиация

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