factors_prod — Mathlib

English

The product of the factors of a is equal to a itself.

Русский

Произведение факторов элемента равно самому элементу.

LaTeX

$$a.factors.prod = a$$

Lean4

@[simp]
theorem factors_prod (a : Associates α) : a.factors.prod = a :=
  by
  rcases Associates.mk_surjective a with ⟨a, rfl⟩
  rcases eq_or_ne a 0 with rfl | ha
  · simp
  · simp [ha, prod_mk, mk_eq_mk_iff_associated, UniqueFactorizationMonoid.factors_prod, -Quotient.eq]

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