irreducible — Mathlib

English

If p is associated to q and p is irreducible, then q is irreducible.

Русский

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

LaTeX

$$$$\mathrm{Associated}(p,q) \land \mathrm{Irreducible}(p) \Rightarrow \mathrm{Irreducible}(q).$$$$

Lean4

protected theorem irreducible [Monoid M] {p q : M} (h : p ~ᵤ q) (hp : Irreducible p) : Irreducible q :=
  ⟨mt h.symm.isUnit hp.1,
    let ⟨u, hu⟩ := h
    fun a b hab =>
    have hpab : p = a * (b * (u⁻¹ : Mˣ)) :=
      calc
        p = p * u * (u⁻¹ : Mˣ) := by simp
        _ = _ := by rw [hu]; simp [hab, mul_assoc]
    (hp.isUnit_or_isUnit hpab).elim Or.inl fun ⟨v, hv⟩ => Or.inr ⟨v * u, by simp [hv]⟩⟩

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