zero_cpow_eq_iff — Mathlib

English

a = 0^x iff (x ≠ 0 and a = 0) or (x = 0 and a = 1).

Русский

a = 0^x тогда и только если (x ≠ 0 и a = 0) или (x = 0 и a = 1).

LaTeX

$$$$ a = 0^{x} \iff (x \neq 0 \land a = 0) \lor (x = 0 \land a = 1). $$$$

Lean4

theorem zero_cpow_eq_iff {x : ℂ} {a : ℂ} : (0 : ℂ) ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 :=
  by
  constructor
  · intro hyp
    simp only [cpow_def, if_true] at hyp
    grind
  · rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)
    · exact zero_cpow h
    · exact cpow_zero _

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