associates_irreducible — Mathlib

English

The associates of v.asIdeal form an irreducible element in the factorization, i.e., Associates.mk(v.asIdeal) is irreducible.

Русский

Ассоциаты v.asIdeal образуют ирредуцируемый элемент в разложении; Associates.mk(v.asIdeal) ирредуцируем.

LaTeX

$$Irreducible(Associates.mk(v.asIdeal))$$

Lean4

theorem associates_irreducible : Irreducible <| Associates.mk v.asIdeal :=
  Associates.irreducible_mk.mpr v.irreducible

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