irreducible_iff_prime_of_exists_prime_factors

English

Under standard hypotheses, irreducible elements coincide with primes.

Русский

При обычных условиях ирредуцируемые элементы совпадают с простыми.

LaTeX

$$$\forall p:\, \alpha,\; \mathrm{Irreducible}(p) \Rightarrow \mathrm{Prime}(p).$$$

Lean4

theorem irreducible_iff_prime_of_exists_prime_factors {p : α} : Irreducible p ↔ Prime p :=
  by
  by_cases hp0 : p = 0
  · simp [hp0]
  refine ⟨fun h => ?_, Prime.irreducible⟩
  obtain ⟨f, hf⟩ := pf p hp0
  obtain ⟨q, hq, rfl⟩ := prime_factors_irreducible h hf
  rw [hq.prime_iff]
  exact hf.1 q (Multiset.mem_singleton_self _)

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