pow_eq_iff — Mathlib

English

Let p,a,k be natural with p prime: a^k = p ↔ a = p ∧ k = 1.

Русский

Пусть p — простое. Тогда a^k = p эквивалентно a = p и k = 1.

LaTeX

$$$$ \forall p,a,k \in \mathbb{N},\ \text{Prime}(p) \rightarrow (a^k = p \iff a = p \land k = 1). $$$$

Lean4

theorem pow_eq_iff {p a k : ℕ} (hp : p.Prime) : a ^ k = p ↔ a = p ∧ k = 1 :=
  by
  refine ⟨fun h => ?_, fun h => by rw [h.1, h.2, pow_one]⟩
  rw [← h] at hp
  rw [← h, hp.eq_one_of_pow, eq_self_iff_true, _root_.and_true, pow_one]

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