normalize_eq

Mathlib.Algebra.GCDMonoid.Basic

URI: https://scilib.ai/kg/mathlib#normalize_eq

English

In a cancellative commutative monoid with unique units, normalize x = x for all x.

Русский

В поглощающе-коммутативном монпейде с уникальными единицами нормализация x равна x для всех x.

LaTeX

$$$$ \\text{normalize}(x) = x. $$$$

Lean4

@[simp]
theorem normalize_eq (x : α) : normalize x = x :=
  mul_one x

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

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

Разделы

Аффилиация

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