liftNormal_commutes — Mathlib

English

The restriction map from the automorphism group of E to that of K₁ is surjective.

Русский

Отображение ограничения из автоморфизмов E на K₁ образует сюръективное отображение.

LaTeX

$$Function.Surjective (AlgEquiv.restrictNormalHom K₁ : (E ≃ₐ[F] E) → K₁ ≃ₐ[F] K₁)$$

Lean4

@[simp]
theorem liftNormal_commutes [Normal F E] (x : K₁) : ϕ.liftNormal E (algebraMap K₁ E x) = algebraMap K₂ E (ϕ x) :=
  -- We have to specify one `Algebra` instance by unification, not synthesis.

  @AlgHom.commutes K₁ E E _ _ _ _ (_) _ _

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