isIntegral_gen

Mathlib.RingTheory.PowerBasis

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

English

The generator pb.gen is integral over A.

Русский

Генератор pb.gen интегрирован над A.

LaTeX

$$IsIntegral A pb.gen$$

Lean4

theorem isIntegral_gen (pb : PowerBasis A S) : IsIntegral A pb.gen :=
  ⟨minpolyGen pb, minpolyGen_monic pb, aeval_minpolyGen pb⟩

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

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

Разделы

Аффилиация

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