Module

SeparableClosedRange.lean

Nyll.ValuedFieldTheory.Valuation.Completion.SeparableClosedRange

1 declaration indexed from sourceView source ↗

Module documentation

Separable elements lie in an embedded separably closed field

An embedding from a separably closed field contains every element that is separable over the common base, without any algebraicity assumption on the ambient extension or on the separably closed field over that base.

Imports2

Mathlib.FieldTheory.IsSepClosed
Mathlib.Algebra.Algebra.Tower

Imported by3

theorem

mem_fieldRange_of_isSeparable_of_isSepClosed

L25 ↗

ValuationTheory.Completion.mem_fieldRange_of_isSeparable_of_isSepClosed

Documentation

An element separable over the common base lies in the image of every embedding from a separably closed field.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ValuationTheory.Completion
variable {K S E : Type*} [Field K] [Field S] [Field E]
  [Algebra K S] [Algebra K E] [IsSepClosed S]

Lean source · statement

theorem mem_fieldRange_of_isSeparable_of_isSepClosed
    (i : S →ₐ[K] E) {x : E} (hx : IsSeparable K x) : x ∈ i.fieldRange

Module documentation

Separable elements lie in an embedded separably closed field

Declarations

mem_fieldRange_of_isSeparable_of_isSepClosed