algEquiv_self

Mathlib.RingTheory.IsAdjoinRoot

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

English

For any z ∈ R[X], h.algEquiv h'(h.map z) = h'.map z.

Русский

Для любого z∈R[X], h.algEquiv h'(h.map z) = h'.map z.

LaTeX

$$$h.algEquiv h'(h.map z) = h'.map z$$$

Lean4

@[simp]
theorem algEquiv_self : h.algEquiv h = AlgEquiv.refl := by ext; simp [algEquiv_def]

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

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

Разделы

Аффилиация

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