restrictScalars_injective — Mathlib

English

restrictScalars K is an injective map from IntermediateField L' L to IntermediateField K L.

Русский

restrictScalars K инъективно отображает IntermediateField L' L в IntermediateField K L.

LaTeX

$$$\\operatorname{Injective}(\\mathrm{restrictScalars}(K))$$$

Lean4

theorem restrictScalars_injective :
    Function.Injective (restrictScalars K : IntermediateField L' L → IntermediateField K L) := fun U V H =>
  ext fun x => by rw [← mem_restrictScalars K, H, mem_restrictScalars]

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