toAlgebra

Mathlib.FieldTheory.IntermediateField.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.toAlgebra

English

An algebra structure on L induces an algebra structure on S via the intermediate-field construction.

Русский

Алгебраическая структура над L порождает структуру над S через конструкцию промежуточного поля.

LaTeX

$$$\\text{Algebra } S$ induced by $\\text{Algebra } L$$$

Lean4

instance toAlgebra : Algebra S L :=
  inferInstanceAs (Algebra S.toSubalgebra L)

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

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

Разделы

Аффилиация

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