Theorems · Theorem · commutative algebra

Valuation.IsEquiv.comap

∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {S : Type u_7}
  [inst_3 : Ring S] (f : S →+* R), v₁.IsEquiv v₂ → (Valuation.comap f v₁).IsEquiv (Valuation.comap f v₂)

comap preserves equivalence.

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingLinearOrderedCommMonoidWithZeroLinearOrderedCommMonoidWithZeroRing