mk_normalize

Mathlib.Algebra.GCDMonoid.Basic

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

English

mk(normalize x) = mk(x)

Русский

mk(normalize x) = mk(x)

LaTeX

$$$ Associates.mk (normalize x) = Associates.mk x. $$$

Lean4

theorem mk_normalize (x : α) : Associates.mk (normalize x) = Associates.mk x :=
  Associates.mk_eq_mk_iff_associated.2 (normalize_associated _)

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

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

Разделы

Аффилиация

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