extendScalars_injective — Mathlib

English

As before, the map E ↦ extendScalars(E) is injective on the family of intermediate fields between F and L.

Русский

Как и прежде, отображение E ↦ extendScalars(E) инъективно на семейство промежуточных полей между F и L.

LaTeX

$$$\\forall E,E'\\big( F \\le E \\land F \\le E' \\rightarrow (extendScalars(E) = extendScalars(E') \\rightarrow E = E') \\big)$$$

Lean4

theorem extendScalars_injective :
    Function.Injective fun E : { E : IntermediateField K L // F ≤ E } ↦ extendScalars E.2 :=
  (extendScalars.orderIso F).injective

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