Theorems · Theorem · commutative algebra

Valuation.isClosed_valuationSubring

∀ {Γ₀ : Type u_3} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_4} [inst_1 : Field K] [inst_2 : ValuativeRel K]
  [inst_3 : TopologicalSpace K] [IsValuativeTopology K] (v : Valuation K Γ₀) [v.Compatible],
  IsClosed ↑v.valuationSubring

For any valuation v compatible with the valuative relation on a field K, the valuation subring defined by v is closed in the valuative topology.

Defined in

Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Cited by

0 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderedCommGroupWithZeroFieldValuativeRelTopologicalSpaceIsValuativeTopologyValuation.Compatible