comap — Mathlib

English

The comap of a subfield S ⊆ L along a RingHom f: K →+* L is a subfield of K.

Русский

Обратное по подполю S через кольцевой гомоморфизм f: K →+* L образует подполе подполе K.

LaTeX

$$$ \text{comap}(S) \text{ is a subfield of } K $$$

Lean4

/-- The preimage of a subfield along a ring homomorphism is a subfield. -/
def comap (s : Subfield L) : Subfield K :=
  { s.toSubring.comap f with
    inv_mem' := fun x hx =>
      show f x⁻¹ ∈ s by
        rw [map_inv₀ f]
        exact s.inv_mem hx }

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