isGalois — Mathlib

English

A (random) homomorphism from a separable extension L of K into a separably closed extension M of K is defined noncomputably as lift.

Русский

Гомоморфизм из сепарабельного расширения L над K в сепаровенно замкнутое расширение M над K определяется невычислимым образом как lift.

LaTeX

$$IsSepClosed.lift : AlgHom K L M$$

Lean4

instance (priority := 100) isGalois [Algebra k K] [IsSepClosure k K] : IsGalois k K
    where
  to_isSeparable := IsSepClosure.separable
  to_normal.toIsAlgebraic := inferInstance
  to_normal.splits' x := (IsSepClosure.sep_closed k).splits_codomain _ (Algebra.IsSeparable.isSeparable k x)

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