prime_of_isPrimal — Mathlib

English

If an element is irreducible and primal, then it is prime.

Русский

Если элемент несводим и прималь, то он прост.

LaTeX

$$irreducible a \land IsPrimal a \Rightarrow Prime a$$

Lean4

theorem prime_of_isPrimal {a : M} (irr : Irreducible a) (primal : IsPrimal a) : Prime a :=
  ⟨irr.ne_zero, irr.not_isUnit, fun a b dvd ↦
    by
    obtain ⟨d₁, d₂, h₁, h₂, rfl⟩ := primal dvd
    exact (of_irreducible_mul irr).symm.imp (·.mul_right_dvd.mpr h₁) (·.mul_left_dvd.mpr h₂)⟩

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