restrict — Mathlib

English

There is an algebra isomorphism between F and the restricted intermediate field inside E: restrict_algEquiv(h) : F ≃ₐ[K] ↥(IntermediateField.restrict h).

Русский

Существует алгебраическое изоморфизм между F и ограниченным промежуточным полем внутри E: restrict_algEquiv(h).

LaTeX

$$$F \\cong_K \\mathrm{IntermediateField}(K,E) \\text{ via } \\text{restrict\_algEquiv}(h)$$$

Lean4

/-- If `F ≤ E` are two intermediate fields of `L / K`, then `F` is also an intermediate field of
`E / K`. It is an inverse of `IntermediateField.lift`, and can be viewed as a dual to
`IntermediateField.extendScalars`.
-/
def restrict : IntermediateField K E :=
  (IntermediateField.inclusion h).fieldRange

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