count_reducible

Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

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

English

If p is not irreducible, then its count is zero.

Русский

Если p не является ирредуцируемым, то счёт p равен 0.

LaTeX

$$$\mathrm{count}(p) = 0$ if $\lnot\mathrm{Irreducible}(p)$.$$

Lean4

theorem count_reducible (hp : ¬Irreducible p) : count p = 0 :=
  dif_neg hp

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

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

Разделы

Аффилиация

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