instDecidablePredMemSetCarrierOfNormalOfDecidableEqOfFintypeAlgEquiv

English

If K ⊆ L is a normal extension and the automorphism group L ≃ₐ[K] L is finite, then for every c the membership predicate x ↦ x ∈ c.carrier is decidable.

Русский

Если расширение K ⊆ L нормальное, а множество(K–алгебравных) автоморфизмов L относительно K конечно, то для каждого c принадлежность элемента x к носителю c.carrier подлежит разрешению.

LaTeX

$$$ (\\text{Normal } K L) \\; \\Rightarrow \\; (\\text{Decidable}(x \\in c.carrier)) $$$

Lean4

instance [Normal K L] [DecidableEq L] [Fintype (L ≃ₐ[K] L)] (c : ConjRootClass K L) : DecidablePred (· ∈ c.carrier) :=
  fun x ↦ decidable_of_iff (mk K x = c) (by simp)

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