Module

DiscreteEquivalence.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteEquivalence

1 declaration indexed from sourceView source ↗

Module documentation

Discrete rank-one valuations under equivalence

Equivalent valuations on a field have the same discrete rank-one property.

Imports2

Mathlib.RingTheory.Valuation.Discrete.Basic
Mathlib.GroupTheory.SpecificGroups.Cyclic

Imported by3

Nyll.ValuedFieldTheory.Valuation.All
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.ProlongationDiscrete
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteNormCompleteExtension

theorem

isRankOneDiscrete

L19 ↗

Valuation.IsEquiv.isRankOneDiscrete

Documentation

Equivalent field valuations have the same discrete rank-one property.

Source context 1 command

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

namespace Valuation

Lean source · statement

theorem IsEquiv.isRankOneDiscrete
    {K Γ Δ : Type*} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
    {v : Valuation K Γ} {w : Valuation K Δ} (h : v.IsEquiv w)
    [v.IsRankOneDiscrete] : w.IsRankOneDiscrete

Module documentation

Discrete rank-one valuations under equivalence

Declarations

isRankOneDiscrete