mk_toAlgEquivAux — Mathlib

English

If g is an element of the limit, then the constructed element equals the limit-projection to a corresponding subfield element.

Русский

Если g принадлежит пределу, то сконструированный элемент совпадает с проекцией-предельной функции к соответствующему элементу подполя.

LaTeX

$$mk_toAlgEquivAux g x L hx' hx$$

Lean4

theorem mk_toAlgEquivAux [IsGalois k K] (g : limit (asProfiniteGaloisGroupFunctor k K)) (x : K)
    (L : FiniteGaloisIntermediateField k K) (hx' : toAlgEquivAux g x ∈ L.toIntermediateField)
    (hx : x ∈ L.toIntermediateField) : (⟨toAlgEquivAux g x, hx'⟩ : L.toIntermediateField) = proj L g ⟨x, hx⟩ := by
  rw [Subtype.eq_iff, Subtype.coe_mk, toAlgEquivAux_eq_proj_of_mem]

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