factors_mk

Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

URI: https://scilib.ai/kg/mathlib#Associates.factors_mk

English

If a ≠ 0, then the factors of mk a equal the factors' of a.

Русский

Если a ≠ 0, то множитель факторов mk a равен factors' a.

LaTeX

$$(Associates.mk a).factors = WithTop.some (Associates.factors' a)$$

Lean4

@[simp]
theorem factors_mk (a : α) (h : a ≠ 0) : (Associates.mk a).factors = factors' a := by
  classical
  apply dif_neg
  apply mt mk_eq_zero.1 h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru