restrictScalars — Mathlib

English

Given a tower of field extensions with E ⊆ L, interpret E as a K-intermediate field of L.

Русский

Дана башня полей L/↦E/↦L'/K; трактуем E как K-промежуточное поле над L.

LaTeX

$$$\\text{restrictScalars}(E) : \\text{IntermediateField } K L$$$

Lean4

/-- Given a tower `L / ↥E / L' / K` of field extensions, where `E` is an `L'`-intermediate field of
`L`, reinterpret `E` as a `K`-intermediate field of `L`. -/
def restrictScalars (E : IntermediateField L' L) : IntermediateField K L :=
  { E.toSubfield, E.toSubalgebra.restrictScalars K with carrier := E.carrier }

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