Theorems · Theorem · commutative algebra

AddValuation.IsEquiv.comap

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

comap preserves equivalence.

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderedAddCommMonoidWithTopLinearOrderedAddCommMonoidWithTopRingRing