extendScalars — Mathlib

English

If F ≤ E are two intermediate fields of L over K, then E can be regarded as an intermediate field of L over F.

Русский

Если F ≤ E — два промежуточных поля L/K, то E можно рассматривать как промежуточное поле L/F.

LaTeX

$$$F \\le E \\Rightarrow E \\in \\mathrm{IntermediateField}(F,L)$$$

Lean4

/-- If `F ≤ E` are two intermediate fields of `L / K`, then `E` is also an intermediate field of
`L / F`. It can be viewed as an inverse to `IntermediateField.restrictScalars`. -/
def extendScalars : IntermediateField F L :=
  Subfield.extendScalars (show F.toSubfield ≤ E.toSubfield from h)

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