dvd_iff_eq — Mathlib

English

For a prime p and a ≠ 1, the divisibility a | p holds if and only if p = a.

Русский

Для простого p и a ≠ 1 выполняется: a делит p тогда и только тогда, когда p = a.

LaTeX

$$$$ \text{Prime}(p) \quad \land \quad a \neq 1 \Rightarrow (a \mid p \iff p = a). $$$$

Lean4

theorem dvd_iff_eq {p a : ℕ} (hp : p.Prime) (a1 : a ≠ 1) : a ∣ p ↔ p = a :=
  by
  refine ⟨?_, by rintro rfl; rfl⟩
  rintro ⟨j, rfl⟩
  rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)
  · exact mul_one _
  · exact (a1 rfl).elim

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