count_self

Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

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

← MathLib Explorer

English

For an irreducible p, the count of p in p.factors equals 1.

Русский

Для неприводимого p число копий p в p.factors равно 1.

LaTeX

$$$$\\mathrm{count}(p, p.factors) = 1.$$$$

Lean4

theorem count_self [Nontrivial α] {p : Associates α} (hp : Irreducible p) : p.count p.factors = 1 := by
  simp [factors_self hp, Associates.count_some hp]

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

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

Разделы

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

Аффилиация

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