aeval_val_eq_zero

Mathlib.RingTheory.Extension.Generators

URI: https://scilib.ai/kg/mathlib#Algebra.Generators.aeval_val_eq_zero

English

If x lies in the kernel, then the evaluation aeval at x gives zero.

Русский

Если x принадлежит ядру, то применение aeval к x даёт 0.

LaTeX

$$$x\\in\\ker(P) \\Rightarrow \\mathrm{aeval}_P(x)=0$$$

Lean4

theorem aeval_val_eq_zero {x} (hx : x ∈ P.ker) : aeval P.val x = 0 := by rwa [← algebraMap_apply]

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

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

Разделы

Аффилиация

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