epow_eq_zero_iff — Mathlib

English

x^y = 0 iff x = 0 and y ≠ 0.

Русский

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

LaTeX

$$$ \forall x,y \in \mathbb{N}_\infty,\; x^y = 0 \iff x = 0 \wedge y \neq 0.$$$

Lean4

theorem epow_eq_zero_iff : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0 :=
  by
  refine ⟨fun h ↦ ⟨?_, fun y_0 ↦ ?_⟩, fun h ↦ h.1.symm ▸ zero_epow h.2⟩
  · by_contra x_0
    exact (one_le_iff_ne_zero.1 (one_le_epow (y := y) x_0) h).rec
  · rw [y_0, epow_zero] at h; contradiction

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