Theorems · Theorem · field theory

Valuation.norm_def

∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀)
  [hv : v.RankOne] {x : L}, v.norm x = ↑((Valuation.RankOne.hom v) (v.restrict x))

Defined in

Mathlib.Topology.Algebra.Valued.NormedValued

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderedCommGroupWithZeroValuation.RankOne