instCoeSortType — Mathlib

English

The collection of finite Galois intermediate fields can be regarded as a type via a canonical coercion.

Русский

Коллекцию конечных галуа-помежуточных полей можно рассматривать как тип через каноническое преобразование.

LaTeX

$$There is a coercion $\mathrm{FiniteGaloisIntermediateField}(k,K) \to \mathrm{Type}$ realizing it as a subtype.$$

Lean4

instance : CoeSort (FiniteGaloisIntermediateField k K) (Type _) where coe L := L.toIntermediateField

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