zero_pow

Mathlib.Algebra.GroupWithZero.Basic

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

English

In a MonoidWithZero, 0^n = 0 for n ≠ 0.

Русский

В MonoidWithZero, 0^n = 0 при n ≠ 0.

LaTeX

$$∀ {n : Nat}, n ≠ 0 → (0 : M₀) ^ n = 0$$

Lean4

@[simp]
theorem zero_pow : ∀ {n : ℕ}, n ≠ 0 → (0 : M₀) ^ n = 0
  | n + 1, _ => by rw [pow_succ, mul_zero]

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

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

Разделы

Аффилиация

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