isAtom_iff — Mathlib

English

Let M be a CancelCommMonoidWithZero. For every p in the Associates of M with p ≠ 0, p is an atom if and only if p is irreducible.

Русский

Пусть M — отменимый коммутативный моноид с нулём. Для каждого p ∈ Associates(M) при p ≠ 0 выполняется: p является атомом тогда и только тогда, когда p неприводим.

LaTeX

$$$p \in \mathrm{Associates}(M),\ p \neq 0 \ \Longrightarrow\ (\mathrm{IsAtom}(p) \iff \mathrm{Irreducible}(p))$$$

Lean4

theorem isAtom_iff {p : Associates M} (h₁ : p ≠ 0) : IsAtom p ↔ Irreducible p :=
  ⟨fun hp =>
    ⟨by simpa only [Associates.isUnit_iff_eq_one] using hp.1, fun a b h =>
      (hp.le_iff.mp ⟨_, h⟩).casesOn (fun ha => Or.inl (a.isUnit_iff_eq_one.mpr ha)) fun ha =>
        Or.inr
          (show IsUnit b by
            rw [ha] at h
            apply isUnit_of_associated_mul (show Associated (p * b) p by conv_rhs => rw [h]) h₁)⟩,
    fun hp =>
    ⟨by simpa only [Associates.isUnit_iff_eq_one, Associates.bot_eq_one] using hp.1, fun b ⟨⟨a, hab⟩, hb⟩ =>
      (hp.isUnit_or_isUnit hab).casesOn
        (fun hb => show b = ⊥ by rwa [Associates.isUnit_iff_eq_one, ← Associates.bot_eq_one] at hb) fun ha =>
        absurd (show p ∣ b from ⟨(ha.unit⁻¹ : Units _), by rw [hab, mul_assoc, IsUnit.mul_val_inv ha, mul_one]⟩) hb⟩⟩

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