Theorems · Theorem · commutative algebra

AddValuation.IsEquiv.map

∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedAddCommMonoidWithTop Γ₀]
  [inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀] [inst_2 : Ring R] {v v' : AddValuation R Γ₀} (f : Γ₀ →+ Γ'₀)
  (ht : f ⊤ = ⊤) (hf : Monotone ⇑f),
  Function.Injective ⇑f → v.IsEquiv v' → (AddValuation.map f ht hf v).IsEquiv (AddValuation.map f ht hf v')

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

LinearOrderedAddCommMonoidWithTopLinearOrderedAddCommMonoidWithTopRing