algEquiv_root

Mathlib.RingTheory.IsAdjoinRoot

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

English

The symmetry of the IsAdjoinRoot algebra is given by (h.algEquiv h').symm = h'.algEquiv h.

Русский

Симметрия изоморфизма IsAdjoinRoot задаётся равенством (h.algEquiv h').symm = h'.algEquiv h.

LaTeX

$$$ (h.algEquiv h').\mathrm{symm} = h'.algEquiv h $$$

Lean4

@[simp]
theorem algEquiv_root : h.algEquiv h' h.root = h'.root := by simp [algEquiv_def]

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

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

Разделы

Аффилиация

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