Theorems · Theorem · commutative algebra

AddValuation.top_iff

∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] [Nontrivial Γ₀]
  (v : AddValuation K Γ₀) {x : K}, v x = ⊤ ↔ x = 0

If v is an additive valuation on a division ring then v(x) = ⊤ iff x = 0.

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

DivisionRingLinearOrderedAddCommMonoidWithTopNontrivial