Theorems · Theorem · commutative algebra

Valuation.exists_div_eq_of_unit

∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ), ∃ r s, 0 < v r ∧ 0 < v s ∧ v.restrict r / v.restrict s = ↑γ

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingLinearOrderedCommGroupWithZero