extendScalars — Mathlib

English

If F ≤ E ≤ L, extendScalars constructs an intermediate field of L whose elements come from E and whose scalars are restricted to F.

Русский

Если F ≤ E ≤ L, extendScalars строит промежуточное поле L, элементы которого берутся из E, а скаляры ограничены F.

LaTeX

$$$\\text{extendScalars} :\\; \\text{Subfield } F L \\to \\text{IntermediateField } F L$$$

Lean4

/-- If `F ≤ E` are two subfields of `L`, then `E` is also an intermediate field of
`L / F`. It can be viewed as an inverse to `IntermediateField.toSubfield`. -/
def extendScalars : IntermediateField F L :=
  E.toIntermediateField fun ⟨_, hf⟩ ↦ h hf

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