dvd_of_mem_factors

Mathlib.RingTheory.UniqueFactorizationDomain.Defs

URI: https://scilib.ai/kg/mathlib#UniqueFactorizationMonoid.dvd_of_mem_factors

← MathLib Explorer

English

If p ∈ factors a, then p divides a.

Русский

Если элемент p принадлежит разложениям a, то он делит a.

LaTeX

$$$p \in \mathrm{factors}(a) \Rightarrow p \mid a$$$

Lean4

theorem dvd_of_mem_factors {p a : α} (h : p ∈ factors a) : p ∣ a :=
  dvd_trans (Multiset.dvd_prod h) (Associated.dvd (factors_prod (ne_zero_of_mem_factors h)))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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