Theorems · Theorem · commutative algebra

WithVal.valueGroupEquiv_symm_apply

∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀)
  (b : { b // (fun x => x ∈ ↑(MonoidWithZeroHom.ofClass v).valueGroup) b }),
  (WithVal.valueGroupEquiv v).symm b = ⟨↑b, ⋯⟩

Defined in

Mathlib.Topology.Algebra.Valued.WithVal

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderedCommGroupWithZeroRing