primeFactors_eq

Mathlib.RingTheory.Radical

URI: https://scilib.ai/kg/mathlib#Associated.primeFactors_eq

← MathLib Explorer

English

Associated elements have the same prime factor set.

Русский

Связанные элементы имеют одинаковое множество простых факторов.

LaTeX

$$$$ primeFactors(a) = primeFactors(b) \text{ if } a \sim b \ (\text{associated}). $$$$

Lean4

theorem _root_.Associated.primeFactors_eq {a b : M} (h : Associated a b) : primeFactors a = primeFactors b :=
  by
  unfold primeFactors
  rw [h.normalizedFactors_eq]

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

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

Разделы

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

Аффилиация

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