equivAdjoinSimple_gen

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

URI: https://scilib.ai/kg/mathlib#PowerBasis.equivAdjoinSimple_gen

English

The equivalence maps the AdjoinSimple generator to pb.gen; i.e., pb.equivAdjoinSimple (AdjoinSimple.gen K pb.gen) = pb.gen.

Русский

Эквививалентность переводит генератор AdjoinSimple в pb.gen.

LaTeX

$$PowerBasis.equivAdjoinSimple_gen pb$$

Lean4

@[simp]
theorem equivAdjoinSimple_gen (pb : PowerBasis K L) : pb.equivAdjoinSimple (AdjoinSimple.gen K pb.gen) = pb.gen :=
  equivOfMinpoly_gen _ pb _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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