X_eq_normalize

Mathlib.Algebra.Polynomial.FieldDivision

URI: https://scilib.ai/kg/mathlib#Polynomial.X_eq_normalize

English

The indeterminate X is unchanged by normalization: X = normalize X.

Русский

Неопределённый X не изменяется нормализацией: X = normalize X.

LaTeX

$$$X = \operatorname{normalize}(X).$$$

Lean4

theorem X_eq_normalize : (X : Polynomial R) = normalize X := by
  simp only [normalize_apply, normUnit_X, Units.val_one, mul_one]

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

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

Разделы

Аффилиация

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