ValuationTheory.DiscreteValuationField.ValuedExtension.isDefectless_of_moduleFinite
A valued extension of discretely valued fields is defectless when its target valuation ring is finite over the base valuation ring.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v w x
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]Lean source · statement
theorem isDefectless_of_moduleFinite
(base : DVF.{u, v} K) (target : DVF.{w, x} L)
[base.valuation.HasExtension target.valuation]
[Module.Finite base.valuationSubring target.valuationSubring]
[IsScalarTower base.valuationSubring target.valuationSubring L] :
IsDefectless base target