isIntegral_algebra

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

URI: https://scilib.ai/kg/mathlib#IsIntegralClosure.isIntegral_algebra

English

If A is an integral closure of R in B, then A is an algebra over R.

Русский

Если A — интегральное замыкание R в B, то A является алгеброй над R.

LaTeX

$$$[\text{Algebra}_R A]$$$

Lean4

theorem isIntegral_algebra [Algebra R A] [IsScalarTower R A B] : Algebra.IsIntegral R A :=
  ⟨fun x => IsIntegralClosure.isIntegral R B x⟩

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

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

Разделы

Аффилиация

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