English
The equality 0^x = a holds exactly in two cases: either x ≠ 0 and a = 0, or x = 0 and a = 1.
Русский
Равенство 0^x = a выполняется только в двух случаях: либо x ≠ 0 и a = 0, либо x = 0 и a = 1.
LaTeX
$$$\\forall x,a \\in \\mathbb{R}, \\; 0^x = a \\iff \\; (x \\neq 0 \\land a = 0) \\lor \\ (x = 0 \\land a = 1)$$$
Lean4
theorem zero_rpow_eq_iff {x : ℝ} {a : ℝ} : 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 :=
by
constructor
· intro hyp
simp only [rpow_def, Complex.ofReal_zero] at hyp
by_cases h : x = 0
· subst h
simp only [Complex.one_re, Complex.ofReal_zero, Complex.cpow_zero] at hyp
exact Or.inr ⟨rfl, hyp.symm⟩
· rw [Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)] at hyp
exact Or.inl ⟨h, hyp.symm⟩
· rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)
· exact zero_rpow h
· exact rpow_zero _
