instCoeIntermediateField

Mathlib.FieldTheory.Galois.GaloisClosure

URI: https://scilib.ai/kg/mathlib#FiniteGaloisIntermediateField.instCoeIntermediateField

English

There is a canonical coercion from FiniteGaloisIntermediateField to IntermediateField.

Русский

Существует каноническое включение из FiniteGaloisIntermediateField в IntermediateField.

LaTeX

$$There exists a canonical coercion $\mathrm{FiniteGaloisIntermediateField}(k,K) \to \mathrm{IntermediateField}(k,K)$.$$

Lean4

instance : Coe (FiniteGaloisIntermediateField k K) (IntermediateField k K) where coe := toIntermediateField

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

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

Разделы

Аффилиация

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