irreducible_iff_prime_iff — Mathlib

English

The equivalence between irreducible and prime is preserved: (∀ a ∈ M, Irreducible a ↔ Prime a) is equivalent to (∀ p ∈ Associates M, Irreducible p ↔ Prime p).

Русский

Эквивалентность между иррeдцируемостью и простотой сохраняется: (∀ a ∈ M, Irreducible a ↔ Prime a) эквивалентно (∀ p ∈ Associates M, Irreducible p ↔ Prime p).

LaTeX

$$$ \big( \forall a \in M, \operatorname{Irreducible}(a) \iff \operatorname{Prime}(a) \big) \iff \big( \forall p \in \mathrm{Associates}(M), \operatorname{Irreducible}(p) \iff \operatorname{Prime}(p) \big) $$$

Lean4

theorem irreducible_iff_prime_iff : (∀ a : M, Irreducible a ↔ Prime a) ↔ ∀ a : Associates M, Irreducible a ↔ Prime a :=
  by simp_rw [forall_associated, irreducible_mk, prime_mk]

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