irreducible_mk — Mathlib

English

DvdNotUnit (Associates.mk a) (Associates.mk b) holds iff DvdNotUnit a b holds.

Русский

DvdNotUnit( mk(a) )( mk(b) ) эквивалентно DvdNotUnit(a,b).

LaTeX

$$$ \text{DvdNotUnit}(\mathrm{mk}(a))(\mathrm{mk}(b)) \iff \text{DvdNotUnit}(a,b) $$$

Lean4

@[simp]
theorem irreducible_mk {a : M} : Irreducible (Associates.mk a) ↔ Irreducible a :=
  by
  simp only [irreducible_iff, isUnit_mk, forall_associated, isUnit_mk, mk_mul_mk, mk_eq_mk_iff_associated,
    Associated.comm (x := a)]
  apply Iff.rfl.and
  constructor
  · rintro h x y rfl
    exact h _ _ <| .refl _
  · rintro h x y ⟨u, rfl⟩
    simpa using h (mul_assoc _ _ _)

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