Theorems · Theorem · commutative algebra

Valuation.extendToLocalization_apply_map_apply

∀ {A : Type u_1} [inst : CommRing A] {Γ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation A Γ)
  {S : Submonoid A} (hS : S ≤ v.supp.primeCompl) (B : Type u_3) [inst_2 : CommRing B] [inst_3 : Algebra A B]
  [inst_4 : IsLocalization S B] (a : A), (v.extendToLocalization hS B) ((algebraMap A B) a) = v a

Defined in

Mathlib.RingTheory.Valuation.ExtendToLocalization

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingLinearOrderedCommGroupWithZeroCommRingAlgebraIsLocalization