fieldEquivOfAlgEquivHom_injective

English

Injectivity of the monotone map sending algebra automorphisms to their induced field automorphisms.

Русский

Инъективность отображения алгебраических автоморфизмов в соответствующие автоморфизмы поля.

LaTeX

$$fieldEquivOfAlgEquivHom_injective K L$$

Lean4

theorem fieldEquivOfAlgEquivHom_injective :
    Function.Injective (fieldEquivOfAlgEquivHom K L : (B ≃ₐ[A] B) →* (L ≃ₐ[K] L)) :=
  by
  intro f g h
  ext b
  simpa using AlgEquiv.ext_iff.mp h (algebraMap B L b)

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