NYLL
Module

HenselianTensorField.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianTensorField
1 declaration indexed from sourceView source ↗

Module documentation

Finite separable extensions after completing a Henselian DVF

The minimal polynomial of a primitive element remains irreducible over the actual valuation completion. The adjoined-root presentation of scalar extension therefore makes the tensor product a field.

Imports4
Imported by3

Declarations

theorem

completionTensor_isField

L30 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.completionTensor_isField
Documentation

Completing a Henselian discretely valued field preserves the field property of every finite separable scalar extension.

Source context 4 commands

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

namespace ValuationTheory.DiscreteValuationField.HenselianDVF
universe u v w
open scoped TensorProduct
variable {K : Type u} [Field K]
Lean source · statement
theorem completionTensor_isField (base : HenselianDVF.{u, v} K)
    (L : Type w) [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L] :
    IsField (base.valuation.Completion ⊗[K] L)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.