rpow_eq_zero_iff — Mathlib

English

For x ∈ NNReal and y ∈ Real, if y ≠ 0, then x^y = 0 iff x = 0.

Русский

Для x ∈ ℝ≥0 и y ∈ ℝ, если y ≠ 0, то x^y = 0 тогда и только тогда, когда x = 0.

LaTeX

$$$\\forall x\\in\\mathbb{R}_{\\ge 0}, \\forall y\\in\\mathbb{R}, \\; y \\neq 0 \\Rightarrow x^{y}=0 \\iff x=0$$$

Lean4

@[simp]
theorem rpow_eq_zero_iff {x : ℝ≥0} {y : ℝ} : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0 :=
  by
  rw [← NNReal.coe_inj, coe_rpow, ← NNReal.coe_eq_zero]
  exact Real.rpow_eq_zero_iff_of_nonneg x.2

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