Theorems · Theorem · commutative algebra

Valuation.restrict_eq_mk

∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R} (hx : v x ≠ 0), v.restrict x = ↑(MonoidWithZeroHom.valueGroup.mk (MonoidWithZeroHom.ofClass v) 1 x ⋯ hx)

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingLinearOrderedCommGroupWithZero