zero_zpow_eq — Mathlib

English

For the zero matrix, (0)^{n} equals 1 if n = 0 and 0 otherwise, for any integer n.

Русский

Для нулевой матрицы (0)^{n} равно 1, если n = 0, и иначе 0, для любого целого n.

LaTeX

$$$$ (0)^{n} = \\begin{cases} 1, & n = 0 \\\\ 0, & n \\neq 0 \\end{cases} \\quad n \\in \\mathbb{Z}. $$$$

Lean4

theorem zero_zpow_eq (n : ℤ) : (0 : M) ^ n = if n = 0 then 1 else 0 :=
  by
  split_ifs with h
  · rw [h, zpow_zero]
  · rw [zero_zpow _ h]

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