zero_zpow — Mathlib

English

For the zero matrix 0, its z-powers are zero whenever the exponent is nonzero: (0)^{z} = 0 for z ≠ 0 in ℤ.

Русский

Нулевая матрица возводится в любую ненулевую z-степень в нуль: (0)^{z} = 0 при z ≠ 0 (z ∈ ℤ).

LaTeX

$$$$ (0)^{z} = 0 \\quad (z \\in \\mathbb{Z}, z \\neq 0). $$$$

Lean4

theorem zero_zpow : ∀ z : ℤ, z ≠ 0 → (0 : M) ^ z = 0
  | (n : ℕ), h => by
    rw [zpow_natCast, zero_pow]
    exact mod_cast h
  | -[n+1], _ => by simp [zero_pow n.succ_ne_zero]

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