one_or_eq_of_le_of_prime — Mathlib

English

If p is prime in Associates M, then for any m with m ≤ p, either m = 1 or m = p.

Русский

Если p прост в Associates(M), то при любом m с m ≤ p либо m = 1, либо m = p.

LaTeX

$$$ \forall p,m \; (\text{Prime}(p) ) \Rightarrow (m \le p \Rightarrow m = 1 \lor m = p) $$$

Lean4

theorem one_or_eq_of_le_of_prime {p m : Associates M} (hp : Prime p) (hle : m ≤ p) : m = 1 ∨ m = p :=
  by
  rcases mk_surjective p with ⟨p, rfl⟩
  rcases mk_surjective m with ⟨m, rfl⟩
  simpa [mk_eq_mk_iff_associated, Associated.comm, -Quotient.eq] using
    (prime_mk.1 hp).irreducible.dvd_iff.mp (mk_le_mk_iff_dvd.1 hle)

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