aeval_repr

Mathlib.RingTheory.AlgebraicIndependent.Defs

URI: https://scilib.ai/kg/mathlib#AlgebraicIndependent.aeval_repr

English

Evaluating the representation map returns the original polynomial element.

Русский

Приении отображения aeval к repr возвращает исходный полином.

LaTeX

$$$\\mathrm{aeval}_{\\text{repr}} = \\mathrm{id}$ на соответствующем представлении$$

Lean4

@[simp]
theorem aeval_repr (p) : aeval x (hx.repr p) = p :=
  Subtype.ext_iff.1 (AlgEquiv.apply_symm_apply hx.aevalEquiv p)

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

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

Разделы

Аффилиация

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