prime — Mathlib

English

If p is prime and p is associated with q, then q is prime.

Русский

Если p — простое и p ассоциировано с q, то q простое.

LaTeX

$$$ [CommMonoidWithZero M] {p q : M} (h : p ~ᵤ q) (hp : Prime p) : Prime q $$$

Lean4

protected theorem prime [CommMonoidWithZero M] {p q : M} (h : p ~ᵤ q) (hp : Prime p) : Prime q :=
  ⟨h.ne_zero_iff.1 hp.ne_zero,
    let ⟨u, hu⟩ := h
    ⟨fun ⟨v, hv⟩ => hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩,
      hu ▸ by
        simp only [Units.isUnit, IsUnit.mul_right_dvd]
        intro a b
        exact hp.dvd_or_dvd⟩⟩

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