eq_one_or_self_of_dvd — Mathlib

English

If p is prime, then for any m with m | p, we have m = 1 or m = p.

Русский

Если p — простое, то для любого m, делящего p, выполняется m = 1 или m = p.

LaTeX

$$$\\\\forall p \\\\forall m \\\\,(\\\\mathrm{Prime}(p) \\\\rightarrow (m \\mid p \\\\rightarrow (m = 1 \\\\lor m = p)))$$$

Lean4

theorem eq_one_or_self_of_dvd {p : ℕ} (pp : p.Prime) (m : ℕ) (hm : m ∣ p) : m = 1 ∨ m = p :=
  by
  obtain ⟨n, hn⟩ := hm
  have := pp.isUnit_or_isUnit hn
  rw [Nat.isUnit_iff, Nat.isUnit_iff] at this
  apply Or.imp_right _ this
  rintro rfl
  rw [hn, mul_one]

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