epow_eq_one_iff — Mathlib

English

x^y = 1 iff x = 1 or y = 0.

Русский

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

LaTeX

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

Lean4

theorem epow_eq_one_iff : x ^ y = 1 ↔ x = 1 ∨ y = 0 :=
  by
  refine ⟨fun h ↦ or_iff_not_imp_right.2 fun y_0 ↦ ?_, fun h ↦ by rcases h with h | h <;> simp [h]⟩
  rcases lt_trichotomy x 1 with x_0 | rfl | x_2
  · rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0] at h; contradiction
  · rfl
  · have := epow_right_mono (one_le_iff_ne_zero.1 x_2.le) (one_le_iff_ne_zero.2 y_0)
    simp only [epow_one, h] at this
    exact (not_lt_of_ge this x_2).rec

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