aeval_root_eq_map

Mathlib.RingTheory.IsAdjoinRoot

URI: https://scilib.ai/kg/mathlib#IsAdjoinRoot.aeval_root_eq_map

English

The aeval of the root of the AdjoinRoot structure equals the mapping h.map as a homomorphism.

Русский

a eал корня структуры IsAdjoinRoot равен отображению h.map как морфизму.

LaTeX

$$$\\operatorname{aeval}_{S} (\\mathrm{root}) = h.map$$$

Lean4

@[simp]
theorem aeval_root_eq_map : aeval h.root = h.map := by ext; simp

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

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

Разделы

Аффилиация

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