mk_dvdNotUnit_mk_iff — Mathlib

English

Irreducible (Associates.mk a) is equivalent to Irreducible a.

Русский

Неразложимость (Associates.mk a) эквивалентна неразложимости a.

LaTeX

$$$ \operatorname{Irreducible}(\mathrm{mk}(a)) \iff \operatorname{Irreducible}(a) $$$

Lean4

@[simp]
theorem mk_dvdNotUnit_mk_iff {a b : M} : DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b :=
  by
  simp only [DvdNotUnit, mk_ne_zero, mk_surjective.exists, isUnit_mk, mk_mul_mk, mk_eq_mk_iff_associated,
    Associated.comm (x := b)]
  refine Iff.rfl.and ?_
  constructor
  · rintro ⟨x, hx, u, rfl⟩
    refine ⟨x * u, ?_, mul_assoc ..⟩
    simpa
  · rintro ⟨x, ⟨hx, rfl⟩⟩
    use x

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